Theorem 3expia 1232

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3expia	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1229	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 124	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005

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 1007

This theorem is referenced by:  ad5ant125  1268  mp3an3  1363  3gencl  2850  moi  3002  ifnebibdc  3670  sotricim  4446  elirr  4665  en2lp  4678  suc11g  4681  3optocl  4830  sefvex  5693  f1oresrab  5844  ovmpos  6179  ov2gf  6180  poxp  6430  brtposg  6487  dfsmo2  6520  smoiun  6534  tfrlemibxssdm  6560  tfr1onlemsucfn  6573  tfr1onlemsucaccv  6574  tfr1onlembxssdm  6576  tfr1onlembfn  6577  tfr1onlemaccex  6581  tfr1onlemres  6582  tfrcllemsucfn  6586  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllembfn  6590  tfrcllemaccex  6594  tfrcllemres  6595  tfrcl  6597  nnsucsssuc  6727  nnaordi  6743  nnawordex  6764  mapvalg  6894  pmvalg  6895  elmapg  6897  xpdom3m  7087  ordiso  7329  ctssdc  7406  pr2ne  7491  ltbtwnnqq  7732  prarloclem4  7815  addlocpr  7853  1idprl  7907  1idpru  7908  ltexprlemrnd  7922  recexprlemrnd  7946  recexprlem1ssl  7950  recexprlem1ssu  7951  recexprlemss1l  7952  recexprlemss1u  7953  aptisr  8096  axpre-apti  8202  ltxrlt  8341  axapti  8346  lttri3  8355  reapti  8855  apreap  8863  msqge0  8892  mulge0  8895  recexap  8929  mulap0b  8931  lt2msq  9162  zaddcl  9619  zdiv  9669  zextlt  9673  prime  9680  uzind2  9693  fzind  9696  lbzbi  9951  xltneg  10172  xlt2add  10216  iocssre  10289  icossre  10290  iccssre  10291  fzen  10380  rebtwn2zlemshrink  10617  qbtwnxr  10621  ioo0  10623  ioom  10624  ico0  10625  ioc0  10626  expclzaplem  10929  expnegzap  10939  expaddzap  10949  expmulzap  10951  omgadd  11170  elovmpowrd  11270  ccatopth2  11413  pfxccatin12  11429  shftuz  11506  cau3lem  11803  climuni  11982  efltim  12388  divalgb  12615  ndvdssub  12620  bitsfzo  12645  dvdsgcd  12712  lcmgcdlem  12778  qredeu  12798  isprm3  12819  prmdvdsexpr  12851  prmexpb  12852  fermltl  12935  coprimeprodsq  12959  pythagtrip  12985  pcpremul  12995  pcdvdsb  13022  pc2dvds  13032  4sqlem12  13104  4sqlem18  13110  ctinf  13198  mulgaddcom  13880  ghmrn  13991  dvdsunit  14274  unitmulclb  14276  lmodvsdi  14476  lss0cl  14534  cnntr  15107  cncnp2m  15113  cnptoprest  15121  lmtopcnp  15132  cnmptcom  15180  hmeof1o  15191  blpnf  15282  blssps  15309  blss  15310  blssec  15320  neibl  15373  climcncf  15466  cnplimcim  15549  plyadd  15633  plymul  15634  upgredg2vtx  16160  bj-peano4  16742  triap  16830