Theorem 3expa 1203

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

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

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 980

This theorem is referenced by:  ad4ant123  1215  ad4ant124  1216  ad4ant134  1217  ad4ant234  1218  3anidm23  1297  mp3an2  1325  mpd3an3  1338  rgen3  2564  moi2  2920  sbc3ie  3038  preq12bg  3775  issod  4321  wepo  4361  reuhypd  4473  funimass4  5569  fvtp1g  5727  f1imass  5778  fcof1o  5793  f1ofveu  5866  f1ocnvfv3  5867  acexmid  5877  2ndrn  6187  frecrdg  6412  oawordriexmid  6474  mapxpen  6851  findcard  6891  findcard2  6892  findcard2s  6893  ltapig  7340  ltanqi  7404  ltmnqi  7405  lt2addnq  7406  lt2mulnq  7407  prarloclemcalc  7504  genpassl  7526  genpassu  7527  prmuloc  7568  ltexprlemm  7602  ltexprlemfl  7611  ltexprlemfu  7613  lteupri  7619  ltaprg  7621  mul4  8092  add4  8121  cnegexlem2  8136  cnegexlem3  8137  2addsub  8174  addsubeq4  8175  muladd  8344  ltleadd  8406  reapmul1  8555  apreim  8563  receuap  8629  p1le  8809  lemul12b  8821  lbinf  8908  zdiv  9344  fzind  9371  fnn0ind  9372  uzss  9551  qmulcl  9640  qreccl  9645  xrlttr  9798  xaddass  9872  icc0r  9929  iooshf  9955  elfz5  10020  elfz0fzfz0  10129  fzind2  10242  ioo0  10263  ico0  10265  ioc0  10266  expnegap0  10531  expineg2  10532  mulexpzap  10563  expsubap  10571  expnbnd  10647  facndiv  10722  bccmpl  10737  bcval5  10746  bcpasc  10749  crim  10870  climshftlemg  11313  2sumeq2dv  11382  hash2iun  11490  2cprodeq2dv  11579  dvdsval3  11801  dvdsnegb  11818  muldvds1  11826  muldvds2  11827  dvdscmul  11828  dvdsmulc  11829  dvds2ln  11834  divalgb  11933  ndvdssub  11938  gcddiv  12023  rpexp1i  12157  phiprmpw  12225  hashgcdeq  12242  pythagtriplem1  12268  pockthg  12358  infpnlem1  12360  4sqlem3  12391  imasaddfnlemg  12741  mndpfo  12846  grplmulf1o  12951  grplactcnv  12979  mulgnn0subcl  13006  mulgsubcl  13007  mulgdir  13025  issubg2m  13059  issubgrpd2  13060  nmzsubg  13080  eqgen  13097  srglmhm  13187  srgrmhm  13188  oppr1g  13263  dvdsrcl2  13279  crngunit  13291  subrgugrp  13372  subsubrg  13377  islmod  13392  lmodvsdir  13413  lmodvsass  13414  lsssubg  13475  lss1d  13481  lidlsubg  13578  lidlsubcl  13579  innei  13824  iscnp4  13879  cnpnei  13880  cnnei  13893  cnconst  13895  ismeti  14007  isxmet2d  14009  elbl2ps  14053  elbl2  14054  xblpnfps  14059  xblpnf  14060  xblm  14078  blininf  14085  blssexps  14090  blssex  14091  blsscls2  14154  metss  14155  metrest  14167  metcn  14175  divcnap  14216  cdivcncfap  14248  lgslem4  14565  lgscllem  14569  lgsneg1  14587  lgsne0  14600