Theorem 3expia 1229

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 1226	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 124	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

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

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 1004

This theorem is referenced by:  ad5ant125  1265  mp3an3  1360  3gencl  2834  moi  2986  ifnebibdc  3648  sotricim  4414  elirr  4633  en2lp  4646  suc11g  4649  3optocl  4797  sefvex  5648  f1oresrab  5800  ovmpos  6128  ov2gf  6129  poxp  6378  brtposg  6400  dfsmo2  6433  smoiun  6447  tfrlemibxssdm  6473  tfr1onlemsucfn  6486  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemaccex  6494  tfr1onlemres  6495  tfrcllemsucfn  6499  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemaccex  6507  tfrcllemres  6508  tfrcl  6510  nnsucsssuc  6638  nnaordi  6654  nnawordex  6675  mapvalg  6805  pmvalg  6806  elmapg  6808  xpdom3m  6993  ordiso  7203  ctssdc  7280  pr2ne  7365  ltbtwnnqq  7602  prarloclem4  7685  addlocpr  7723  1idprl  7777  1idpru  7778  ltexprlemrnd  7792  recexprlemrnd  7816  recexprlem1ssl  7820  recexprlem1ssu  7821  recexprlemss1l  7822  recexprlemss1u  7823  aptisr  7966  axpre-apti  8072  ltxrlt  8212  axapti  8217  lttri3  8226  reapti  8726  apreap  8734  msqge0  8763  mulge0  8766  recexap  8800  mulap0b  8802  lt2msq  9033  zaddcl  9486  zdiv  9535  zextlt  9539  prime  9546  uzind2  9559  fzind  9562  lbzbi  9811  xltneg  10032  xlt2add  10076  iocssre  10149  icossre  10150  iccssre  10151  fzen  10239  rebtwn2zlemshrink  10473  qbtwnxr  10477  ioo0  10479  ioom  10480  ico0  10481  ioc0  10482  expclzaplem  10785  expnegzap  10795  expaddzap  10805  expmulzap  10807  omgadd  11024  elovmpowrd  11113  ccatopth2  11249  pfxccatin12  11265  shftuz  11328  cau3lem  11625  climuni  11804  efltim  12209  divalgb  12436  ndvdssub  12441  bitsfzo  12466  dvdsgcd  12533  lcmgcdlem  12599  qredeu  12619  isprm3  12640  prmdvdsexpr  12672  prmexpb  12673  fermltl  12756  coprimeprodsq  12780  pythagtrip  12806  pcpremul  12816  pcdvdsb  12843  pc2dvds  12853  4sqlem12  12925  4sqlem18  12931  ctinf  13001  mulgaddcom  13683  ghmrn  13794  dvdsunit  14076  unitmulclb  14078  lmodvsdi  14275  lss0cl  14333  cnntr  14899  cncnp2m  14905  cnptoprest  14913  lmtopcnp  14924  cnmptcom  14972  hmeof1o  14983  blpnf  15074  blssps  15101  blss  15102  blssec  15112  neibl  15165  climcncf  15258  cnplimcim  15341  plyadd  15425  plymul  15426  upgredg2vtx  15946  bj-peano4  16318  triap  16397