Theorem 3expa 1193

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  ad4ant123  1205  ad4ant124  1206  ad4ant134  1207  ad4ant234  1208  3anidm23  1287  mp3an2  1315  mpd3an3  1328  rgen3  2552  moi2  2906  sbc3ie  3023  preq12bg  3752  issod  4296  wepo  4336  reuhypd  4448  funimass4  5536  fvtp1g  5692  f1imass  5741  fcof1o  5756  f1ofveu  5829  f1ocnvfv3  5830  acexmid  5840  2ndrn  6148  frecrdg  6372  oawordriexmid  6434  mapxpen  6810  findcard  6850  findcard2  6851  findcard2s  6852  ltapig  7275  ltanqi  7339  ltmnqi  7340  lt2addnq  7341  lt2mulnq  7342  prarloclemcalc  7439  genpassl  7461  genpassu  7462  prmuloc  7503  ltexprlemm  7537  ltexprlemfl  7546  ltexprlemfu  7548  lteupri  7554  ltaprg  7556  mul4  8026  add4  8055  cnegexlem2  8070  cnegexlem3  8071  2addsub  8108  addsubeq4  8109  muladd  8278  ltleadd  8340  reapmul1  8489  apreim  8497  receuap  8562  p1le  8740  lemul12b  8752  lbinf  8839  zdiv  9275  fzind  9302  fnn0ind  9303  uzss  9482  qmulcl  9571  qreccl  9576  xrlttr  9727  xaddass  9801  icc0r  9858  iooshf  9884  elfz5  9948  elfz0fzfz0  10057  fzind2  10170  ioo0  10191  ico0  10193  ioc0  10194  expnegap0  10459  expineg2  10460  mulexpzap  10491  expsubap  10499  expnbnd  10574  facndiv  10648  bccmpl  10663  bcval5  10672  bcpasc  10675  crim  10796  climshftlemg  11239  2sumeq2dv  11308  hash2iun  11416  2cprodeq2dv  11505  dvdsval3  11727  dvdsnegb  11744  muldvds1  11752  muldvds2  11753  dvdscmul  11754  dvdsmulc  11755  dvds2ln  11760  divalgb  11858  ndvdssub  11863  gcddiv  11948  rpexp1i  12082  phiprmpw  12150  hashgcdeq  12167  pythagtriplem1  12193  pockthg  12283  infpnlem1  12285  4sqlem3  12316  innei  12763  iscnp4  12818  cnpnei  12819  cnnei  12832  cnconst  12834  ismeti  12946  isxmet2d  12948  elbl2ps  12992  elbl2  12993  xblpnfps  12998  xblpnf  12999  xblm  13017  blininf  13024  blssexps  13029  blssex  13030  blsscls2  13093  metss  13094  metrest  13106  metcn  13114  divcnap  13155  cdivcncfap  13187  lgslem4  13504  lgscllem  13508  lgsneg1  13526  lgsne0  13539