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  2806  moi  2956  ifnebibdc  3615  sotricim  4371  elirr  4590  en2lp  4603  suc11g  4606  3optocl  4754  sefvex  5599  f1oresrab  5747  ovmpos  6071  ov2gf  6072  poxp  6320  brtposg  6342  dfsmo2  6375  smoiun  6389  tfrlemibxssdm  6415  tfr1onlemsucfn  6428  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfr1onlemaccex  6436  tfr1onlemres  6437  tfrcllemsucfn  6441  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  tfrcllemaccex  6449  tfrcllemres  6450  tfrcl  6452  nnsucsssuc  6580  nnaordi  6596  nnawordex  6617  mapvalg  6747  pmvalg  6748  elmapg  6750  xpdom3m  6931  ordiso  7140  ctssdc  7217  pr2ne  7302  ltbtwnnqq  7530  prarloclem4  7613  addlocpr  7651  1idprl  7705  1idpru  7706  ltexprlemrnd  7720  recexprlemrnd  7744  recexprlem1ssl  7748  recexprlem1ssu  7749  recexprlemss1l  7750  recexprlemss1u  7751  aptisr  7894  axpre-apti  8000  ltxrlt  8140  axapti  8145  lttri3  8154  reapti  8654  apreap  8662  msqge0  8691  mulge0  8694  recexap  8728  mulap0b  8730  lt2msq  8961  zaddcl  9414  zdiv  9463  zextlt  9467  prime  9474  uzind2  9487  fzind  9490  lbzbi  9739  xltneg  9960  xlt2add  10004  iocssre  10077  icossre  10078  iccssre  10079  fzen  10167  rebtwn2zlemshrink  10398  qbtwnxr  10402  ioo0  10404  ioom  10405  ico0  10406  ioc0  10407  expclzaplem  10710  expnegzap  10720  expaddzap  10730  expmulzap  10732  omgadd  10949  elovmpowrd  11037  shftuz  11161  cau3lem  11458  climuni  11637  efltim  12042  divalgb  12269  ndvdssub  12274  bitsfzo  12299  dvdsgcd  12366  lcmgcdlem  12432  qredeu  12452  isprm3  12473  prmdvdsexpr  12505  prmexpb  12506  fermltl  12589  coprimeprodsq  12613  pythagtrip  12639  pcpremul  12649  pcdvdsb  12676  pc2dvds  12686  4sqlem12  12758  4sqlem18  12764  ctinf  12834  mulgaddcom  13515  ghmrn  13626  dvdsunit  13907  unitmulclb  13909  lmodvsdi  14106  lss0cl  14164  cnntr  14730  cncnp2m  14736  cnptoprest  14744  lmtopcnp  14755  cnmptcom  14803  hmeof1o  14814  blpnf  14905  blssps  14932  blss  14933  blssec  14943  neibl  14996  climcncf  15089  cnplimcim  15172  plyadd  15256  plymul  15257  bj-peano4  15928  triap  16005