Theorem 3expia 1231

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

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

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 1006

This theorem is referenced by:  ad5ant125  1267  mp3an3  1362  3gencl  2837  moi  2989  ifnebibdc  3651  sotricim  4420  elirr  4639  en2lp  4652  suc11g  4655  3optocl  4804  sefvex  5661  f1oresrab  5813  ovmpos  6148  ov2gf  6149  poxp  6400  brtposg  6423  dfsmo2  6456  smoiun  6470  tfrlemibxssdm  6496  tfr1onlemsucfn  6509  tfr1onlemsucaccv  6510  tfr1onlembxssdm  6512  tfr1onlembfn  6513  tfr1onlemaccex  6517  tfr1onlemres  6518  tfrcllemsucfn  6522  tfrcllemsucaccv  6523  tfrcllembxssdm  6525  tfrcllembfn  6526  tfrcllemaccex  6530  tfrcllemres  6531  tfrcl  6533  nnsucsssuc  6663  nnaordi  6679  nnawordex  6700  mapvalg  6830  pmvalg  6831  elmapg  6833  xpdom3m  7021  ordiso  7238  ctssdc  7315  pr2ne  7400  ltbtwnnqq  7638  prarloclem4  7721  addlocpr  7759  1idprl  7813  1idpru  7814  ltexprlemrnd  7828  recexprlemrnd  7852  recexprlem1ssl  7856  recexprlem1ssu  7857  recexprlemss1l  7858  recexprlemss1u  7859  aptisr  8002  axpre-apti  8108  ltxrlt  8248  axapti  8253  lttri3  8262  reapti  8762  apreap  8770  msqge0  8799  mulge0  8802  recexap  8836  mulap0b  8838  lt2msq  9069  zaddcl  9522  zdiv  9571  zextlt  9575  prime  9582  uzind2  9595  fzind  9598  lbzbi  9853  xltneg  10074  xlt2add  10118  iocssre  10191  icossre  10192  iccssre  10193  fzen  10281  rebtwn2zlemshrink  10517  qbtwnxr  10521  ioo0  10523  ioom  10524  ico0  10525  ioc0  10526  expclzaplem  10829  expnegzap  10839  expaddzap  10849  expmulzap  10851  omgadd  11069  elovmpowrd  11162  ccatopth2  11305  pfxccatin12  11321  shftuz  11398  cau3lem  11695  climuni  11874  efltim  12280  divalgb  12507  ndvdssub  12512  bitsfzo  12537  dvdsgcd  12604  lcmgcdlem  12670  qredeu  12690  isprm3  12711  prmdvdsexpr  12743  prmexpb  12744  fermltl  12827  coprimeprodsq  12851  pythagtrip  12877  pcpremul  12887  pcdvdsb  12914  pc2dvds  12924  4sqlem12  12996  4sqlem18  13002  ctinf  13072  mulgaddcom  13754  ghmrn  13865  dvdsunit  14148  unitmulclb  14150  lmodvsdi  14347  lss0cl  14405  cnntr  14976  cncnp2m  14982  cnptoprest  14990  lmtopcnp  15001  cnmptcom  15049  hmeof1o  15060  blpnf  15151  blssps  15178  blss  15179  blssec  15189  neibl  15242  climcncf  15335  cnplimcim  15418  plyadd  15502  plymul  15503  upgredg2vtx  16026  bj-peano4  16609  triap  16692