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  2918  sbc3ie  3036  preq12bg  3773  issod  4319  wepo  4359  reuhypd  4471  funimass4  5566  fvtp1g  5724  f1imass  5774  fcof1o  5789  f1ofveu  5862  f1ocnvfv3  5863  acexmid  5873  2ndrn  6183  frecrdg  6408  oawordriexmid  6470  mapxpen  6847  findcard  6887  findcard2  6888  findcard2s  6889  ltapig  7336  ltanqi  7400  ltmnqi  7401  lt2addnq  7402  lt2mulnq  7403  prarloclemcalc  7500  genpassl  7522  genpassu  7523  prmuloc  7564  ltexprlemm  7598  ltexprlemfl  7607  ltexprlemfu  7609  lteupri  7615  ltaprg  7617  mul4  8088  add4  8117  cnegexlem2  8132  cnegexlem3  8133  2addsub  8170  addsubeq4  8171  muladd  8340  ltleadd  8402  reapmul1  8551  apreim  8559  receuap  8625  p1le  8805  lemul12b  8817  lbinf  8904  zdiv  9340  fzind  9367  fnn0ind  9368  uzss  9547  qmulcl  9636  qreccl  9641  xrlttr  9794  xaddass  9868  icc0r  9925  iooshf  9951  elfz5  10016  elfz0fzfz0  10125  fzind2  10238  ioo0  10259  ico0  10261  ioc0  10262  expnegap0  10527  expineg2  10528  mulexpzap  10559  expsubap  10567  expnbnd  10643  facndiv  10718  bccmpl  10733  bcval5  10742  bcpasc  10745  crim  10866  climshftlemg  11309  2sumeq2dv  11378  hash2iun  11486  2cprodeq2dv  11575  dvdsval3  11797  dvdsnegb  11814  muldvds1  11822  muldvds2  11823  dvdscmul  11824  dvdsmulc  11825  dvds2ln  11830  divalgb  11929  ndvdssub  11934  gcddiv  12019  rpexp1i  12153  phiprmpw  12221  hashgcdeq  12238  pythagtriplem1  12264  pockthg  12354  infpnlem1  12356  4sqlem3  12387  imasaddfnlemg  12734  mndpfo  12838  grplmulf1o  12943  grplactcnv  12971  mulgnn0subcl  12995  mulgsubcl  12996  mulgdir  13013  issubg2m  13047  issubgrpd2  13048  nmzsubg  13068  eqgen  13084  srglmhm  13174  srgrmhm  13175  oppr1g  13250  dvdsrcl2  13266  crngunit  13278  subrgugrp  13359  subsubrg  13364  islmod  13379  lmodvsdir  13400  lmodvsass  13401  innei  13633  iscnp4  13688  cnpnei  13689  cnnei  13702  cnconst  13704  ismeti  13816  isxmet2d  13818  elbl2ps  13862  elbl2  13863  xblpnfps  13868  xblpnf  13869  xblm  13887  blininf  13894  blssexps  13899  blssex  13900  blsscls2  13963  metss  13964  metrest  13976  metcn  13984  divcnap  14025  cdivcncfap  14057  lgslem4  14374  lgscllem  14378  lgsneg1  14396  lgsne0  14409