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  2797  moi  2947  ifnebibdc  3605  sotricim  4359  elirr  4578  en2lp  4591  suc11g  4594  3optocl  4742  sefvex  5582  f1oresrab  5730  ovmpos  6050  ov2gf  6051  poxp  6299  brtposg  6321  dfsmo2  6354  smoiun  6368  tfrlemibxssdm  6394  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemaccex  6428  tfrcllemres  6429  tfrcl  6431  nnsucsssuc  6559  nnaordi  6575  nnawordex  6596  mapvalg  6726  pmvalg  6727  elmapg  6729  xpdom3m  6902  ordiso  7111  ctssdc  7188  pr2ne  7271  ltbtwnnqq  7499  prarloclem4  7582  addlocpr  7620  1idprl  7674  1idpru  7675  ltexprlemrnd  7689  recexprlemrnd  7713  recexprlem1ssl  7717  recexprlem1ssu  7718  recexprlemss1l  7719  recexprlemss1u  7720  aptisr  7863  axpre-apti  7969  ltxrlt  8109  axapti  8114  lttri3  8123  reapti  8623  apreap  8631  msqge0  8660  mulge0  8663  recexap  8697  mulap0b  8699  lt2msq  8930  zaddcl  9383  zdiv  9431  zextlt  9435  prime  9442  uzind2  9455  fzind  9458  lbzbi  9707  xltneg  9928  xlt2add  9972  iocssre  10045  icossre  10046  iccssre  10047  fzen  10135  rebtwn2zlemshrink  10360  qbtwnxr  10364  ioo0  10366  ioom  10367  ico0  10368  ioc0  10369  expclzaplem  10672  expnegzap  10682  expaddzap  10692  expmulzap  10694  omgadd  10911  elovmpowrd  10993  shftuz  10999  cau3lem  11296  climuni  11475  efltim  11880  divalgb  12107  ndvdssub  12112  bitsfzo  12137  dvdsgcd  12204  lcmgcdlem  12270  qredeu  12290  isprm3  12311  prmdvdsexpr  12343  prmexpb  12344  fermltl  12427  coprimeprodsq  12451  pythagtrip  12477  pcpremul  12487  pcdvdsb  12514  pc2dvds  12524  4sqlem12  12596  4sqlem18  12602  ctinf  12672  mulgaddcom  13352  ghmrn  13463  dvdsunit  13744  unitmulclb  13746  lmodvsdi  13943  lss0cl  14001  cnntr  14545  cncnp2m  14551  cnptoprest  14559  lmtopcnp  14570  cnmptcom  14618  hmeof1o  14629  blpnf  14720  blssps  14747  blss  14748  blssec  14758  neibl  14811  climcncf  14904  cnplimcim  14987  plyadd  15071  plymul  15072  bj-peano4  15685  triap  15760