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  2786  moi  2935  sotricim  4341  elirr  4558  en2lp  4571  suc11g  4574  3optocl  4722  sefvex  5555  f1oresrab  5701  ovmpos  6019  ov2gf  6020  poxp  6256  brtposg  6278  dfsmo2  6311  smoiun  6325  tfrlemibxssdm  6351  tfr1onlemsucfn  6364  tfr1onlemsucaccv  6365  tfr1onlembxssdm  6367  tfr1onlembfn  6368  tfr1onlemaccex  6372  tfr1onlemres  6373  tfrcllemsucfn  6377  tfrcllemsucaccv  6378  tfrcllembxssdm  6380  tfrcllembfn  6381  tfrcllemaccex  6385  tfrcllemres  6386  tfrcl  6388  nnsucsssuc  6516  nnaordi  6532  nnawordex  6553  mapvalg  6683  pmvalg  6684  elmapg  6686  xpdom3m  6859  ordiso  7064  ctssdc  7141  pr2ne  7220  ltbtwnnqq  7443  prarloclem4  7526  addlocpr  7564  1idprl  7618  1idpru  7619  ltexprlemrnd  7633  recexprlemrnd  7657  recexprlem1ssl  7661  recexprlem1ssu  7662  recexprlemss1l  7663  recexprlemss1u  7664  aptisr  7807  axpre-apti  7913  ltxrlt  8052  axapti  8057  lttri3  8066  reapti  8565  apreap  8573  msqge0  8602  mulge0  8605  recexap  8639  mulap0b  8641  lt2msq  8872  zaddcl  9322  zdiv  9370  zextlt  9374  prime  9381  uzind2  9394  fzind  9397  lbzbi  9645  xltneg  9865  xlt2add  9909  iocssre  9982  icossre  9983  iccssre  9984  fzen  10072  rebtwn2zlemshrink  10283  qbtwnxr  10287  ioo0  10289  ioom  10290  ico0  10291  ioc0  10292  expclzaplem  10574  expnegzap  10584  expaddzap  10594  expmulzap  10596  omgadd  10813  shftuz  10857  cau3lem  11154  climuni  11332  efltim  11737  divalgb  11961  ndvdssub  11966  dvdsgcd  12044  lcmgcdlem  12108  qredeu  12128  isprm3  12149  prmdvdsexpr  12181  prmexpb  12182  fermltl  12265  coprimeprodsq  12288  pythagtrip  12314  pcpremul  12324  pcdvdsb  12351  pc2dvds  12361  4sqlem12  12433  4sqlem18  12439  ctinf  12480  mulgaddcom  13083  ghmrn  13193  dvdsunit  13459  unitmulclb  13461  lmodvsdi  13624  lss0cl  13682  cnntr  14177  cncnp2m  14183  cnptoprest  14191  lmtopcnp  14202  cnmptcom  14250  hmeof1o  14261  blpnf  14352  blssps  14379  blss  14380  blssec  14390  neibl  14443  climcncf  14523  cnplimcim  14588  bj-peano4  15160  triap  15231