Theorem 3expa 1144

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

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

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

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

This theorem is referenced by:  3anidm23  1234  mp3an2  1262  mpd3an3  1275  rgen3  2461  moi2  2799  sbc3ie  2915  preq12bg  3625  issod  4157  wepo  4197  reuhypd  4308  funimass4  5370  fvtp1g  5521  f1imass  5569  fcof1o  5584  f1ofveu  5656  f1ocnvfv3  5657  acexmid  5667  2ndrn  5969  frecrdg  6189  oawordriexmid  6247  mapxpen  6620  findcard  6660  findcard2  6661  findcard2s  6662  ltapig  6960  ltanqi  7024  ltmnqi  7025  lt2addnq  7026  lt2mulnq  7027  prarloclemcalc  7124  genpassl  7146  genpassu  7147  prmuloc  7188  ltexprlemm  7222  ltexprlemfl  7231  ltexprlemfu  7233  lteupri  7239  ltaprg  7241  mul4  7677  add4  7706  cnegexlem2  7721  cnegexlem3  7722  2addsub  7759  addsubeq4  7760  muladd  7925  ltleadd  7987  reapmul1  8135  apreim  8143  receuap  8201  p1le  8373  lemul12b  8385  lbinf  8472  zdiv  8897  fzind  8924  fnn0ind  8925  uzss  9102  qmulcl  9185  qreccl  9190  xrlttr  9328  icc0r  9407  iooshf  9433  elfz5  9495  elfz0fzfz0  9600  fzind2  9713  ioo0  9734  ico0  9736  ioc0  9737  expnegap0  10026  expineg2  10027  mulexpzap  10058  expsubap  10066  expnbnd  10140  facndiv  10210  bccmpl  10225  ibcval5  10234  bcpasc  10237  crim  10355  climshftlemg  10753  2sumeq2dv  10823  hash2iun  10936  dvdsval3  11141  dvdsnegb  11154  muldvds1  11162  muldvds2  11163  dvdscmul  11164  dvdsmulc  11165  dvds2ln  11170  divalgb  11266  ndvdssub  11271  gcddiv  11349  rpexp1i  11474  phiprmpw  11539  hashgcdeq  11545  innei  11926