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  2919  sbc3ie  3037  preq12bg  3774  issod  4320  wepo  4360  reuhypd  4472  funimass4  5567  fvtp1g  5725  f1imass  5775  fcof1o  5790  f1ofveu  5863  f1ocnvfv3  5864  acexmid  5874  2ndrn  6184  frecrdg  6409  oawordriexmid  6471  mapxpen  6848  findcard  6888  findcard2  6889  findcard2s  6890  ltapig  7337  ltanqi  7401  ltmnqi  7402  lt2addnq  7403  lt2mulnq  7404  prarloclemcalc  7501  genpassl  7523  genpassu  7524  prmuloc  7565  ltexprlemm  7599  ltexprlemfl  7608  ltexprlemfu  7610  lteupri  7616  ltaprg  7618  mul4  8089  add4  8118  cnegexlem2  8133  cnegexlem3  8134  2addsub  8171  addsubeq4  8172  muladd  8341  ltleadd  8403  reapmul1  8552  apreim  8560  receuap  8626  p1le  8806  lemul12b  8818  lbinf  8905  zdiv  9341  fzind  9368  fnn0ind  9369  uzss  9548  qmulcl  9637  qreccl  9642  xrlttr  9795  xaddass  9869  icc0r  9926  iooshf  9952  elfz5  10017  elfz0fzfz0  10126  fzind2  10239  ioo0  10260  ico0  10262  ioc0  10263  expnegap0  10528  expineg2  10529  mulexpzap  10560  expsubap  10568  expnbnd  10644  facndiv  10719  bccmpl  10734  bcval5  10743  bcpasc  10746  crim  10867  climshftlemg  11310  2sumeq2dv  11379  hash2iun  11487  2cprodeq2dv  11576  dvdsval3  11798  dvdsnegb  11815  muldvds1  11823  muldvds2  11824  dvdscmul  11825  dvdsmulc  11826  dvds2ln  11831  divalgb  11930  ndvdssub  11935  gcddiv  12020  rpexp1i  12154  phiprmpw  12222  hashgcdeq  12239  pythagtriplem1  12265  pockthg  12355  infpnlem1  12357  4sqlem3  12388  imasaddfnlemg  12735  mndpfo  12839  grplmulf1o  12944  grplactcnv  12972  mulgnn0subcl  12996  mulgsubcl  12997  mulgdir  13015  issubg2m  13049  issubgrpd2  13050  nmzsubg  13070  eqgen  13086  srglmhm  13176  srgrmhm  13177  oppr1g  13252  dvdsrcl2  13268  crngunit  13280  subrgugrp  13361  subsubrg  13366  islmod  13381  lmodvsdir  13402  lmodvsass  13403  innei  13666  iscnp4  13721  cnpnei  13722  cnnei  13735  cnconst  13737  ismeti  13849  isxmet2d  13851  elbl2ps  13895  elbl2  13896  xblpnfps  13901  xblpnf  13902  xblm  13920  blininf  13927  blssexps  13932  blssex  13933  blsscls2  13996  metss  13997  metrest  14009  metcn  14017  divcnap  14058  cdivcncfap  14090  lgslem4  14407  lgscllem  14411  lgsneg1  14429  lgsne0  14442