Theorem 3expa 1205

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  ad4ant123  1217  ad4ant124  1218  ad4ant134  1219  ad4ant234  1220  ad5ant123  1241  3anidm23  1308  mp3an2  1336  mpd3an3  1349  rgen3  2584  moi2  2945  sbc3ie  3063  preq12bg  3804  issod  4355  wepo  4395  reuhypd  4507  funimass4  5614  fvtp1g  5773  f1imass  5824  fcof1o  5839  f1ofveu  5913  f1ocnvfv3  5914  acexmid  5924  2ndrn  6250  frecrdg  6475  oawordriexmid  6537  mapxpen  6918  findcard  6958  findcard2  6959  findcard2s  6960  ltapig  7422  ltanqi  7486  ltmnqi  7487  lt2addnq  7488  lt2mulnq  7489  prarloclemcalc  7586  genpassl  7608  genpassu  7609  prmuloc  7650  ltexprlemm  7684  ltexprlemfl  7693  ltexprlemfu  7695  lteupri  7701  ltaprg  7703  mul4  8175  add4  8204  cnegexlem2  8219  cnegexlem3  8220  2addsub  8257  addsubeq4  8258  muladd  8427  ltleadd  8490  reapmul1  8639  apreim  8647  receuap  8713  p1le  8893  lemul12b  8905  lbinf  8992  zdiv  9431  fzind  9458  fnn0ind  9459  uzss  9639  qmulcl  9728  qreccl  9733  xrlttr  9887  xaddass  9961  icc0r  10018  iooshf  10044  elfz5  10109  elfz0fzfz0  10218  fzind2  10332  ioo0  10366  ico0  10368  ioc0  10369  expnegap0  10656  expineg2  10657  mulexpzap  10688  expsubap  10696  expnbnd  10772  facndiv  10848  bccmpl  10863  bcval5  10872  bcpasc  10875  crim  11040  climshftlemg  11484  2sumeq2dv  11553  hash2iun  11661  2cprodeq2dv  11750  dvdsval3  11973  dvdsnegb  11990  muldvds1  11998  muldvds2  11999  dvdscmul  12000  dvdsmulc  12001  dvds2ln  12006  divalgb  12107  ndvdssub  12112  gcddiv  12211  rpexp1i  12347  phiprmpw  12415  hashgcdeq  12433  pythagtriplem1  12459  pockthg  12551  infpnlem1  12553  4sqlem3  12584  imasaddfnlemg  13016  mndpfo  13140  grplmulf1o  13276  grplactcnv  13304  mulgnn0subcl  13341  mulgsubcl  13342  mulgdir  13360  issubg2m  13395  issubgrpd2  13396  nmzsubg  13416  eqgen  13433  ghmmulg  13462  ghmf1  13479  kerf1ghm  13480  conjghm  13482  srglmhm  13625  srgrmhm  13626  ringlghm  13693  ringrghm  13694  oppr1g  13714  dvdsrcl2  13731  crngunit  13743  subsubrng  13846  subrgugrp  13872  subsubrg  13877  islmod  13923  lmodvsdir  13944  lmodvsass  13945  lsssubg  14009  lss1d  14015  lidlsubg  14118  lidlsubcl  14119  expghmap  14239  mulgghm2  14240  innei  14483  iscnp4  14538  cnpnei  14539  cnnei  14552  cnconst  14554  ismeti  14666  isxmet2d  14668  elbl2ps  14712  elbl2  14713  xblpnfps  14718  xblpnf  14719  xblm  14737  blininf  14744  blssexps  14749  blssex  14750  blsscls2  14813  metss  14814  metrest  14826  metcn  14834  divcnap  14885  cdivcncfap  14924  dvply1  15085  lgslem4  15328  lgscllem  15332  lgsneg1  15350  lgsne0  15363