Theorem 3expia 1205

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

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

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 980

This theorem is referenced by:  mp3an3  1326  3gencl  2773  moi  2922  sotricim  4325  elirr  4542  en2lp  4555  suc11g  4558  3optocl  4706  sefvex  5538  f1oresrab  5683  ovmpos  6000  ov2gf  6001  poxp  6235  brtposg  6257  dfsmo2  6290  smoiun  6304  tfrlemibxssdm  6330  tfr1onlemsucfn  6343  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemaccex  6351  tfr1onlemres  6352  tfrcllemsucfn  6356  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemaccex  6364  tfrcllemres  6365  tfrcl  6367  nnsucsssuc  6495  nnaordi  6511  nnawordex  6532  mapvalg  6660  pmvalg  6661  elmapg  6663  xpdom3m  6836  ordiso  7037  ctssdc  7114  pr2ne  7193  ltbtwnnqq  7416  prarloclem4  7499  addlocpr  7537  1idprl  7591  1idpru  7592  ltexprlemrnd  7606  recexprlemrnd  7630  recexprlem1ssl  7634  recexprlem1ssu  7635  recexprlemss1l  7636  recexprlemss1u  7637  aptisr  7780  axpre-apti  7886  ltxrlt  8025  axapti  8030  lttri3  8039  reapti  8538  apreap  8546  msqge0  8575  mulge0  8578  recexap  8612  mulap0b  8614  lt2msq  8845  zaddcl  9295  zdiv  9343  zextlt  9347  prime  9354  uzind2  9367  fzind  9370  lbzbi  9618  xltneg  9838  xlt2add  9882  iocssre  9955  icossre  9956  iccssre  9957  fzen  10045  rebtwn2zlemshrink  10256  qbtwnxr  10260  ioo0  10262  ioom  10263  ico0  10264  ioc0  10265  expclzaplem  10546  expnegzap  10556  expaddzap  10566  expmulzap  10568  omgadd  10784  shftuz  10828  cau3lem  11125  climuni  11303  efltim  11708  divalgb  11932  ndvdssub  11937  dvdsgcd  12015  lcmgcdlem  12079  qredeu  12099  isprm3  12120  prmdvdsexpr  12152  prmexpb  12153  fermltl  12236  coprimeprodsq  12259  pythagtrip  12285  pcpremul  12295  pcdvdsb  12321  pc2dvds  12331  ctinf  12433  mulgaddcom  13012  dvdsunit  13286  unitmulclb  13288  lmodvsdi  13406  lss0cl  13460  cnntr  13810  cncnp2m  13816  cnptoprest  13824  lmtopcnp  13835  cnmptcom  13883  hmeof1o  13894  blpnf  13985  blssps  14012  blss  14013  blssec  14023  neibl  14076  climcncf  14156  cnplimcim  14221  bj-peano4  14792  triap  14862