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  5650  f1oresrab  5802  ovmpos  6134  ov2gf  6135  poxp  6384  brtposg  6406  dfsmo2  6439  smoiun  6453  tfrlemibxssdm  6479  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemaccex  6513  tfrcllemres  6514  tfrcl  6516  nnsucsssuc  6646  nnaordi  6662  nnawordex  6683  mapvalg  6813  pmvalg  6814  elmapg  6816  xpdom3m  7001  ordiso  7214  ctssdc  7291  pr2ne  7376  ltbtwnnqq  7613  prarloclem4  7696  addlocpr  7734  1idprl  7788  1idpru  7789  ltexprlemrnd  7803  recexprlemrnd  7827  recexprlem1ssl  7831  recexprlem1ssu  7832  recexprlemss1l  7833  recexprlemss1u  7834  aptisr  7977  axpre-apti  8083  ltxrlt  8223  axapti  8228  lttri3  8237  reapti  8737  apreap  8745  msqge0  8774  mulge0  8777  recexap  8811  mulap0b  8813  lt2msq  9044  zaddcl  9497  zdiv  9546  zextlt  9550  prime  9557  uzind2  9570  fzind  9573  lbzbi  9823  xltneg  10044  xlt2add  10088  iocssre  10161  icossre  10162  iccssre  10163  fzen  10251  rebtwn2zlemshrink  10485  qbtwnxr  10489  ioo0  10491  ioom  10492  ico0  10493  ioc0  10494  expclzaplem  10797  expnegzap  10807  expaddzap  10817  expmulzap  10819  omgadd  11036  elovmpowrd  11126  ccatopth2  11265  pfxccatin12  11281  shftuz  11344  cau3lem  11641  climuni  11820  efltim  12225  divalgb  12452  ndvdssub  12457  bitsfzo  12482  dvdsgcd  12549  lcmgcdlem  12615  qredeu  12635  isprm3  12656  prmdvdsexpr  12688  prmexpb  12689  fermltl  12772  coprimeprodsq  12796  pythagtrip  12822  pcpremul  12832  pcdvdsb  12859  pc2dvds  12869  4sqlem12  12941  4sqlem18  12947  ctinf  13017  mulgaddcom  13699  ghmrn  13810  dvdsunit  14092  unitmulclb  14094  lmodvsdi  14291  lss0cl  14349  cnntr  14915  cncnp2m  14921  cnptoprest  14929  lmtopcnp  14940  cnmptcom  14988  hmeof1o  14999  blpnf  15090  blssps  15117  blss  15118  blssec  15128  neibl  15181  climcncf  15274  cnplimcim  15357  plyadd  15441  plymul  15442  upgredg2vtx  15962  bj-peano4  16401  triap  16485