Theorem 3expia 1236

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

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

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 1011

This theorem is referenced by:  ad5ant125  1272  mp3an3  1367  3gencl  2856  moi  3009  ifnebibdc  3686  sotricim  4466  elirr  4686  en2lp  4699  suc11g  4702  3optocl  4851  sefvex  5714  f1oresrab  5867  ovmpos  6205  ov2gf  6206  poxp  6461  brtposg  6518  dfsmo2  6551  smoiun  6565  tfrlemibxssdm  6591  tfr1onlemsucfn  6604  tfr1onlemsucaccv  6605  tfr1onlembxssdm  6607  tfr1onlembfn  6608  tfr1onlemaccex  6612  tfr1onlemres  6613  tfrcllemsucfn  6617  tfrcllemsucaccv  6618  tfrcllembxssdm  6620  tfrcllembfn  6621  tfrcllemaccex  6625  tfrcllemres  6626  tfrcl  6628  nnsucsssuc  6758  nnaordi  6774  nnawordex  6795  mapvalg  6925  pmvalg  6926  elmapg  6928  xpdom3m  7125  ordiso  7369  ctssdc  7446  pr2ne  7531  ltbtwnnqq  7775  prarloclem4  7858  addlocpr  7896  1idprl  7950  1idpru  7951  ltexprlemrnd  7965  recexprlemrnd  7989  recexprlem1ssl  7993  recexprlem1ssu  7994  recexprlemss1l  7995  recexprlemss1u  7996  aptisr  8139  axpre-apti  8245  ltxrlt  8384  axapti  8389  lttri3  8398  reapti  8900  apreap  8908  msqge0  8937  mulge0  8940  recexap  8974  mulap0b  8976  lt2msq  9209  zaddcl  9666  zdiv  9716  zextlt  9720  prime  9727  uzind2  9740  fzind  9743  lbzbi  9998  xltneg  10220  xlt2add  10264  iocssre  10337  icossre  10338  iccssre  10339  fzen  10429  rebtwn2zlemshrink  10669  qbtwnxr  10673  ioo0  10675  ioom  10676  ico0  10677  ioc0  10678  expclzaplem  10981  expnegzap  10991  expaddzap  11001  expmulzap  11003  omgadd  11223  elovmpowrd  11327  ccatopth2  11470  pfxccatin12  11486  shftuz  11563  cau3lem  11861  climuni  12040  efltim  12446  divalgb  12673  ndvdssub  12678  bitsfzo  12703  dvdsgcd  12770  lcmgcdlem  12836  qredeu  12856  isprm3  12877  prmdvdsexpr  12909  prmexpb  12910  fermltl  12993  coprimeprodsq  13017  pythagtrip  13043  pcpremul  13053  pcdvdsb  13080  pc2dvds  13090  4sqlem12  13162  4sqlem18  13168  ballotfilemirc  13256  ctinf  13302  mulgaddcom  13929  ghmrn  14040  dvdsunit  14395  unitmulclb  14397  lmodvsdi  14623  lss0cl  14681  cnntr  15252  cncnp2m  15258  cnptoprest  15266  lmtopcnp  15277  cnmptcom  15325  hmeof1o  15336  blpnf  15427  blssps  15454  blss  15455  blssec  15465  neibl  15518  climcncf  15611  cnplimcim  15694  plyadd  15778  plymul  15779  upgredg2vtx  16306  lealltlt2  16669  dichmul0or  16677  bj-peano4  16898  triap  16986