Theorem 3expa 1198

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

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 1197	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 254	1 |- ( ( ( ph /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  ad4ant123  1210  ad4ant124  1211  ad4ant134  1212  ad4ant234  1213  3anidm23  1292  mp3an2  1320  mpd3an3  1333  rgen3  2557  moi2  2911  sbc3ie  3028  preq12bg  3760  issod  4304  wepo  4344  reuhypd  4456  funimass4  5547  fvtp1g  5704  f1imass  5753  fcof1o  5768  f1ofveu  5841  f1ocnvfv3  5842  acexmid  5852  2ndrn  6162  frecrdg  6387  oawordriexmid  6449  mapxpen  6826  findcard  6866  findcard2  6867  findcard2s  6868  ltapig  7300  ltanqi  7364  ltmnqi  7365  lt2addnq  7366  lt2mulnq  7367  prarloclemcalc  7464  genpassl  7486  genpassu  7487  prmuloc  7528  ltexprlemm  7562  ltexprlemfl  7571  ltexprlemfu  7573  lteupri  7579  ltaprg  7581  mul4  8051  add4  8080  cnegexlem2  8095  cnegexlem3  8096  2addsub  8133  addsubeq4  8134  muladd  8303  ltleadd  8365  reapmul1  8514  apreim  8522  receuap  8587  p1le  8765  lemul12b  8777  lbinf  8864  zdiv  9300  fzind  9327  fnn0ind  9328  uzss  9507  qmulcl  9596  qreccl  9601  xrlttr  9752  xaddass  9826  icc0r  9883  iooshf  9909  elfz5  9973  elfz0fzfz0  10082  fzind2  10195  ioo0  10216  ico0  10218  ioc0  10219  expnegap0  10484  expineg2  10485  mulexpzap  10516  expsubap  10524  expnbnd  10599  facndiv  10673  bccmpl  10688  bcval5  10697  bcpasc  10700  crim  10822  climshftlemg  11265  2sumeq2dv  11334  hash2iun  11442  2cprodeq2dv  11531  dvdsval3  11753  dvdsnegb  11770  muldvds1  11778  muldvds2  11779  dvdscmul  11780  dvdsmulc  11781  dvds2ln  11786  divalgb  11884  ndvdssub  11889  gcddiv  11974  rpexp1i  12108  phiprmpw  12176  hashgcdeq  12193  pythagtriplem1  12219  pockthg  12309  infpnlem1  12311  4sqlem3  12342  mndpfo  12674  innei  12957  iscnp4  13012  cnpnei  13013  cnnei  13026  cnconst  13028  ismeti  13140  isxmet2d  13142  elbl2ps  13186  elbl2  13187  xblpnfps  13192  xblpnf  13193  xblm  13211  blininf  13218  blssexps  13223  blssex  13224  blsscls2  13287  metss  13288  metrest  13300  metcn  13308  divcnap  13349  cdivcncfap  13381  lgslem4  13698  lgscllem  13702  lgsneg1  13720  lgsne0  13733