Theorem 3expia 1208

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

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

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 983

This theorem is referenced by:  ad5ant125  1244  mp3an3  1339  3gencl  2811  moi  2963  ifnebibdc  3625  sotricim  4388  elirr  4607  en2lp  4620  suc11g  4623  3optocl  4771  sefvex  5620  f1oresrab  5768  ovmpos  6092  ov2gf  6093  poxp  6341  brtposg  6363  dfsmo2  6396  smoiun  6410  tfrlemibxssdm  6436  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemaccex  6457  tfr1onlemres  6458  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemaccex  6470  tfrcllemres  6471  tfrcl  6473  nnsucsssuc  6601  nnaordi  6617  nnawordex  6638  mapvalg  6768  pmvalg  6769  elmapg  6771  xpdom3m  6954  ordiso  7164  ctssdc  7241  pr2ne  7326  ltbtwnnqq  7563  prarloclem4  7646  addlocpr  7684  1idprl  7738  1idpru  7739  ltexprlemrnd  7753  recexprlemrnd  7777  recexprlem1ssl  7781  recexprlem1ssu  7782  recexprlemss1l  7783  recexprlemss1u  7784  aptisr  7927  axpre-apti  8033  ltxrlt  8173  axapti  8178  lttri3  8187  reapti  8687  apreap  8695  msqge0  8724  mulge0  8727  recexap  8761  mulap0b  8763  lt2msq  8994  zaddcl  9447  zdiv  9496  zextlt  9500  prime  9507  uzind2  9520  fzind  9523  lbzbi  9772  xltneg  9993  xlt2add  10037  iocssre  10110  icossre  10111  iccssre  10112  fzen  10200  rebtwn2zlemshrink  10433  qbtwnxr  10437  ioo0  10439  ioom  10440  ico0  10441  ioc0  10442  expclzaplem  10745  expnegzap  10755  expaddzap  10765  expmulzap  10767  omgadd  10984  elovmpowrd  11072  ccatopth2  11208  pfxccatin12  11224  shftuz  11243  cau3lem  11540  climuni  11719  efltim  12124  divalgb  12351  ndvdssub  12356  bitsfzo  12381  dvdsgcd  12448  lcmgcdlem  12514  qredeu  12534  isprm3  12555  prmdvdsexpr  12587  prmexpb  12588  fermltl  12671  coprimeprodsq  12695  pythagtrip  12721  pcpremul  12731  pcdvdsb  12758  pc2dvds  12768  4sqlem12  12840  4sqlem18  12846  ctinf  12916  mulgaddcom  13597  ghmrn  13708  dvdsunit  13989  unitmulclb  13991  lmodvsdi  14188  lss0cl  14246  cnntr  14812  cncnp2m  14818  cnptoprest  14826  lmtopcnp  14837  cnmptcom  14885  hmeof1o  14896  blpnf  14987  blssps  15014  blss  15015  blssec  15025  neibl  15078  climcncf  15171  cnplimcim  15254  plyadd  15338  plymul  15339  upgredg2vtx  15852  bj-peano4  16090  triap  16170