Theorem 3expa 835

Description: Exportation from triple to double conjunction.

Hypothesis

Ref	Expression
3exp.1	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
3expa	|- (((ph /\ ps) /\ ch) -> th)

Proof of Theorem 3expa

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 834	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp31 362	1 |- (((ph /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 777

This theorem is referenced by:  mp3an2 906  mp3an3 907  mpd3an3 919  rgen3 1727  mouniss 2897  f1ocnvfv1 3885  f1ocnvfv2 3886  f1ofveu 3889  isotr 3904  isotrALT 3905  tfrlem11 3928  curry1f 4106  oalimcl 4201  oeordsuc 4228  oelim2 4229  nneob 4262  mapenlem1 4496  ltapi 5049  add4t 5357  cnegextlem2 5365  cnegextlem3 5366  2addsubt 5408  mul4t 5439  muladdt 5440  xrlttrt 5572  ltleaddt 5664  divasst 5755  div23t 5756  div12t 5758  divsubdirtOLD 5784  divmuldivt 5789  divadddivt 5793  divdivdivt 5794  divdiv23t 5801  p1let 5826  lemul12ait 5851  lemul12itOLD 5852  lediv1tOLD 5861  lemuldivtOLD 5884  ltdiv23t 5901  lediv23t 5902  nndivt 5968  lbinfm 6057  nnreclt 6081  xrsupsslem 6085  xrinfmsslem 6086  supxrunb1 6098  zbtwnre 6230  fladdzt 6253  qnegclt 6278  qmulclt 6279  qrecclt 6281  qdivclt 6282  qbtwnre 6286  seq1rn 6330  ioo0t 6376  iooint 6380  iooss1 6381  iooss2 6382  ioojoint 6424  uzss 6439  elfz5t 6482  fznn0subt 6506  fzss1t 6511  fzrevralt 6527  recexpt 6603  expsubt 6606  divexpt 6607  expord2t 6612  expmwordit 6614  exple1t 6615  absmaxt 6904  seq1ublem 6918  caure 6934  cauim 6935  facndivt 6950  faclbnd4lem4 6958  faclbnd4 6959  faclbnd5 6960  bccl2t 6978  2sumeq2dv 7001  fsum1ps 7025  fsumsplit 7027  fsumrev2 7037  fsumshftm 7039  fsum2mul 7044  clm3 7086  climaddlem3 7123  climmullem5 7131  climmullem8 7134  climabslem 7155  caucvglem5 7168  cvgcmp3c 7193  isum1p 7213  isumreclt 7217  isummulc1ALT 7220  cvgratlem1 7257  cvgratlem2 7258  cvgratlem5 7261  abspef01tlub 7402  acdc2lem2 7497  acdc5lem2 7500  infpnlem1 7514  infxpdom 7579  infxp 7580  infmap2 7590  tgss2t 7643  basgen2t 7645  2basgent 7647  subtop 7650  elcls2 7709  innei 7740  cnco 7772  cnsscnp 7776  cncnp 7782  cncnp2 7783  ismsi 7805  ismeti 7806  bl2in 7847  blin 7856  blss 7857  ssbl 7859  opni3 7870  metcnp 7891  metcnp2 7892  metcn 7893  cncfmet 7909  bl2ioo 7915  lmnn 7939  lmuni 7955  lmss 7957  lmle 7964  metelcls 7969  metcnp4lem2 7973  metcn4 7975  xplm 7979  iscms2lem4 7996  iscms2lem5 7997  lmcau 8000  grpidinvlem3 8054  isgrp2i 8079  ring2 8152  isvci 8204  va1cnlem 8348  ipval2lem2 8357  ipval2lem5 8363  sspival 8400  sspimsval 8402  nmoub3i 8439  isblo2 8446  0lno 8453  nmo0 8454  blocni 8468  isph 8484  sspph 8518  ipblnfi 8519  minveclem27 8574  shftefif1olem 8743  relogeftb 8767  hvadd4t 8907  hiassdit 8959  ocsh 9158  occllem6 9180  projlem2 9189  projlem25 9212  projlem26 9213  projlem28 9215  pjeqt 9244  chj4t 9460  spansncol 9493  pjspansnt 9502  pjjs 9647  hoadd4t 9712  homco1t 9729  homulasst 9730  hoadddit 9731  hoadddirt 9732  nmopub2tALT 9835  unoplint 9846  counopt 9847  nmfnleub2t 9852  adjvalvalt 9863  hmoplint 9868  bralnfnt 9874  brafnmult 9877  homco2t 9903  lnopm 9927  lnopco 9930  hmopmt 9948  hmopcot 9950  nmophm 9963  lnfncnbdt 9994  cnlnadjlem2 10003  adjlnopt 10021  adjmult 10027  branmfnt 10040  kbass5t 10055  kbass6t 10056  leop2t 10059  leopmulit 10068  pjima 10106  atcvatlem 10315  irredlem2 10321  mdsymlem3 10335  mdsymlem5 10337  sumdmdi 10345  sumdmdlem 10348  cdj3lem2a 10366  cdj3lem2b 10367  cdj3lem3a 10369  cdj3 10371

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 779

Copyright terms: Public domain