Theorem 3expia 1207

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

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

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 982

This theorem is referenced by:  ad5ant125  1243  mp3an3  1337  3gencl  2794  moi  2943  ifnebibdc  3600  sotricim  4354  elirr  4573  en2lp  4586  suc11g  4589  3optocl  4737  sefvex  5575  f1oresrab  5723  ovmpos  6042  ov2gf  6043  poxp  6285  brtposg  6307  dfsmo2  6340  smoiun  6354  tfrlemibxssdm  6380  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemaccex  6401  tfr1onlemres  6402  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemaccex  6414  tfrcllemres  6415  tfrcl  6417  nnsucsssuc  6545  nnaordi  6561  nnawordex  6582  mapvalg  6712  pmvalg  6713  elmapg  6715  xpdom3m  6888  ordiso  7095  ctssdc  7172  pr2ne  7252  ltbtwnnqq  7475  prarloclem4  7558  addlocpr  7596  1idprl  7650  1idpru  7651  ltexprlemrnd  7665  recexprlemrnd  7689  recexprlem1ssl  7693  recexprlem1ssu  7694  recexprlemss1l  7695  recexprlemss1u  7696  aptisr  7839  axpre-apti  7945  ltxrlt  8085  axapti  8090  lttri3  8099  reapti  8598  apreap  8606  msqge0  8635  mulge0  8638  recexap  8672  mulap0b  8674  lt2msq  8905  zaddcl  9357  zdiv  9405  zextlt  9409  prime  9416  uzind2  9429  fzind  9432  lbzbi  9681  xltneg  9902  xlt2add  9946  iocssre  10019  icossre  10020  iccssre  10021  fzen  10109  rebtwn2zlemshrink  10322  qbtwnxr  10326  ioo0  10328  ioom  10329  ico0  10330  ioc0  10331  expclzaplem  10634  expnegzap  10644  expaddzap  10654  expmulzap  10656  omgadd  10873  elovmpowrd  10955  shftuz  10961  cau3lem  11258  climuni  11436  efltim  11841  divalgb  12066  ndvdssub  12071  dvdsgcd  12149  lcmgcdlem  12215  qredeu  12235  isprm3  12256  prmdvdsexpr  12288  prmexpb  12289  fermltl  12372  coprimeprodsq  12395  pythagtrip  12421  pcpremul  12431  pcdvdsb  12458  pc2dvds  12468  4sqlem12  12540  4sqlem18  12546  ctinf  12587  mulgaddcom  13216  ghmrn  13327  dvdsunit  13608  unitmulclb  13610  lmodvsdi  13807  lss0cl  13865  cnntr  14393  cncnp2m  14399  cnptoprest  14407  lmtopcnp  14418  cnmptcom  14466  hmeof1o  14477  blpnf  14568  blssps  14595  blss  14596  blssec  14606  neibl  14659  climcncf  14739  cnplimcim  14821  plyadd  14897  plymul  14898  bj-peano4  15447  triap  15519