Theorem 3expia 1205

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

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

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 980

This theorem is referenced by:  mp3an3  1326  3gencl  2772  moi  2921  sotricim  4324  elirr  4541  en2lp  4554  suc11g  4557  3optocl  4705  sefvex  5537  f1oresrab  5682  ovmpos  5998  ov2gf  5999  poxp  6233  brtposg  6255  dfsmo2  6288  smoiun  6302  tfrlemibxssdm  6328  tfr1onlemsucfn  6341  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfr1onlemaccex  6349  tfr1onlemres  6350  tfrcllemsucfn  6354  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemaccex  6362  tfrcllemres  6363  tfrcl  6365  nnsucsssuc  6493  nnaordi  6509  nnawordex  6530  mapvalg  6658  pmvalg  6659  elmapg  6661  xpdom3m  6834  ordiso  7035  ctssdc  7112  pr2ne  7191  ltbtwnnqq  7414  prarloclem4  7497  addlocpr  7535  1idprl  7589  1idpru  7590  ltexprlemrnd  7604  recexprlemrnd  7628  recexprlem1ssl  7632  recexprlem1ssu  7633  recexprlemss1l  7634  recexprlemss1u  7635  aptisr  7778  axpre-apti  7884  ltxrlt  8023  axapti  8028  lttri3  8037  reapti  8536  apreap  8544  msqge0  8573  mulge0  8576  recexap  8610  mulap0b  8612  lt2msq  8843  zaddcl  9293  zdiv  9341  zextlt  9345  prime  9352  uzind2  9365  fzind  9368  lbzbi  9616  xltneg  9836  xlt2add  9880  iocssre  9953  icossre  9954  iccssre  9955  fzen  10043  rebtwn2zlemshrink  10254  qbtwnxr  10258  ioo0  10260  ioom  10261  ico0  10262  ioc0  10263  expclzaplem  10544  expnegzap  10554  expaddzap  10564  expmulzap  10566  omgadd  10782  shftuz  10826  cau3lem  11123  climuni  11301  efltim  11706  divalgb  11930  ndvdssub  11935  dvdsgcd  12013  lcmgcdlem  12077  qredeu  12097  isprm3  12118  prmdvdsexpr  12150  prmexpb  12151  fermltl  12234  coprimeprodsq  12257  pythagtrip  12283  pcpremul  12293  pcdvdsb  12319  pc2dvds  12329  ctinf  12431  mulgaddcom  13007  dvdsunit  13281  unitmulclb  13283  lmodvsdi  13401  cnntr  13728  cncnp2m  13734  cnptoprest  13742  lmtopcnp  13753  cnmptcom  13801  hmeof1o  13812  blpnf  13903  blssps  13930  blss  13931  blssec  13941  neibl  13994  climcncf  14074  cnplimcim  14139  bj-peano4  14710  triap  14780