Theorem 3expa 1185

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

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

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 965

This theorem is referenced by:  ad4ant123  1197  ad4ant124  1198  ad4ant134  1199  ad4ant234  1200  3anidm23  1279  mp3an2  1307  mpd3an3  1320  rgen3  2544  moi2  2893  sbc3ie  3010  preq12bg  3736  issod  4279  wepo  4319  reuhypd  4431  funimass4  5519  fvtp1g  5675  f1imass  5724  fcof1o  5739  f1ofveu  5812  f1ocnvfv3  5813  acexmid  5823  2ndrn  6131  frecrdg  6355  oawordriexmid  6417  mapxpen  6793  findcard  6833  findcard2  6834  findcard2s  6835  ltapig  7258  ltanqi  7322  ltmnqi  7323  lt2addnq  7324  lt2mulnq  7325  prarloclemcalc  7422  genpassl  7444  genpassu  7445  prmuloc  7486  ltexprlemm  7520  ltexprlemfl  7529  ltexprlemfu  7531  lteupri  7537  ltaprg  7539  mul4  8007  add4  8036  cnegexlem2  8051  cnegexlem3  8052  2addsub  8089  addsubeq4  8090  muladd  8259  ltleadd  8321  reapmul1  8470  apreim  8478  receuap  8543  p1le  8720  lemul12b  8732  lbinf  8819  zdiv  9252  fzind  9279  fnn0ind  9280  uzss  9459  qmulcl  9546  qreccl  9551  xrlttr  9702  xaddass  9773  icc0r  9830  iooshf  9856  elfz5  9920  elfz0fzfz0  10025  fzind2  10138  ioo0  10159  ico0  10161  ioc0  10162  expnegap0  10427  expineg2  10428  mulexpzap  10459  expsubap  10467  expnbnd  10541  facndiv  10613  bccmpl  10628  bcval5  10637  bcpasc  10640  crim  10758  climshftlemg  11199  2sumeq2dv  11268  hash2iun  11376  2cprodeq2dv  11465  dvdsval3  11687  dvdsnegb  11703  muldvds1  11711  muldvds2  11712  dvdscmul  11713  dvdsmulc  11714  dvds2ln  11719  divalgb  11815  ndvdssub  11820  gcddiv  11902  rpexp1i  12028  phiprmpw  12096  hashgcdeq  12113  innei  12563  iscnp4  12618  cnpnei  12619  cnnei  12632  cnconst  12634  ismeti  12746  isxmet2d  12748  elbl2ps  12792  elbl2  12793  xblpnfps  12798  xblpnf  12799  xblm  12817  blininf  12824  blssexps  12829  blssex  12830  blsscls2  12893  metss  12894  metrest  12906  metcn  12914  divcnap  12955  cdivcncfap  12987