Theorem 3expa 1227

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

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

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 1004

This theorem is referenced by:  ad4ant123  1239  ad4ant124  1240  ad4ant134  1241  ad4ant234  1242  ad5ant123  1263  3anidm23  1331  mp3an2  1359  mpd3an3  1372  rgen3  2617  moi2  2985  sbc3ie  3103  2if2dc  3643  preq12bg  3854  issod  4414  wepo  4454  reuhypd  4566  funimass4  5692  fvtp1g  5857  f1imass  5910  fcof1o  5925  f1ofveu  6001  f1ocnvfv3  6002  acexmid  6012  2ndrn  6341  frecrdg  6569  oawordriexmid  6633  mapxpen  7029  findcard  7070  findcard2  7071  findcard2s  7072  ltapig  7548  ltanqi  7612  ltmnqi  7613  lt2addnq  7614  lt2mulnq  7615  prarloclemcalc  7712  genpassl  7734  genpassu  7735  prmuloc  7776  ltexprlemm  7810  ltexprlemfl  7819  ltexprlemfu  7821  lteupri  7827  ltaprg  7829  mul4  8301  add4  8330  cnegexlem2  8345  cnegexlem3  8346  2addsub  8383  addsubeq4  8384  muladd  8553  ltleadd  8616  reapmul1  8765  apreim  8773  receuap  8839  p1le  9019  lemul12b  9031  lbinf  9118  zdiv  9558  fzind  9585  fnn0ind  9586  uzss  9767  qmulcl  9861  qreccl  9866  xrlttr  10020  xaddass  10094  icc0r  10151  iooshf  10177  elfz5  10242  elfz0fzfz0  10351  fzind2  10475  ioo0  10509  ico0  10511  ioc0  10512  expnegap0  10799  expineg2  10800  mulexpzap  10831  expsubap  10839  expnbnd  10915  facndiv  10991  bccmpl  11006  bcval5  11015  bcpasc  11018  ccatrn  11176  swrdspsleq  11238  swrdccat2  11242  ccatpfx  11272  pfxccat1  11273  swrdswrd  11276  cats1un  11292  crim  11409  climshftlemg  11853  2sumeq2dv  11922  hash2iun  12030  2cprodeq2dv  12119  dvdsval3  12342  dvdsnegb  12359  muldvds1  12367  muldvds2  12368  dvdscmul  12369  dvdsmulc  12370  dvds2ln  12375  divalgb  12476  ndvdssub  12481  gcddiv  12580  rpexp1i  12716  phiprmpw  12784  hashgcdeq  12802  pythagtriplem1  12828  pockthg  12920  infpnlem1  12922  4sqlem3  12953  imasaddfnlemg  13387  mndpfo  13511  grplmulf1o  13647  grplactcnv  13675  mulgnn0subcl  13712  mulgsubcl  13713  mulgdir  13731  issubg2m  13766  issubgrpd2  13767  nmzsubg  13787  eqgen  13804  ghmmulg  13833  ghmf1  13850  kerf1ghm  13851  conjghm  13853  srglmhm  13996  srgrmhm  13997  ringlghm  14064  ringrghm  14065  oppr1g  14085  dvdsrcl2  14103  crngunit  14115  subsubrng  14218  subrgugrp  14244  subsubrg  14249  islmod  14295  lmodvsdir  14316  lmodvsass  14317  lsssubg  14381  lss1d  14387  lidlsubg  14490  lidlsubcl  14491  expghmap  14611  mulgghm2  14612  innei  14877  iscnp4  14932  cnpnei  14933  cnnei  14946  cnconst  14948  ismeti  15060  isxmet2d  15062  elbl2ps  15106  elbl2  15107  xblpnfps  15112  xblpnf  15113  xblm  15131  blininf  15138  blssexps  15143  blssex  15144  blsscls2  15207  metss  15208  metrest  15220  metcn  15228  divcnap  15279  cdivcncfap  15318  dvply1  15479  lgslem4  15722  lgscllem  15726  lgsneg1  15744  lgsne0  15757  uspgr2wlkeq  16162