Theorem 3expia 1208

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

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

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 983

This theorem is referenced by:  ad5ant125  1244  mp3an3  1339  3gencl  2806  moi  2956  ifnebibdc  3615  sotricim  4370  elirr  4589  en2lp  4602  suc11g  4605  3optocl  4753  sefvex  5597  f1oresrab  5745  ovmpos  6069  ov2gf  6070  poxp  6318  brtposg  6340  dfsmo2  6373  smoiun  6387  tfrlemibxssdm  6413  tfr1onlemsucfn  6426  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfr1onlemaccex  6434  tfr1onlemres  6435  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcllemaccex  6447  tfrcllemres  6448  tfrcl  6450  nnsucsssuc  6578  nnaordi  6594  nnawordex  6615  mapvalg  6745  pmvalg  6746  elmapg  6748  xpdom3m  6929  ordiso  7138  ctssdc  7215  pr2ne  7300  ltbtwnnqq  7528  prarloclem4  7611  addlocpr  7649  1idprl  7703  1idpru  7704  ltexprlemrnd  7718  recexprlemrnd  7742  recexprlem1ssl  7746  recexprlem1ssu  7747  recexprlemss1l  7748  recexprlemss1u  7749  aptisr  7892  axpre-apti  7998  ltxrlt  8138  axapti  8143  lttri3  8152  reapti  8652  apreap  8660  msqge0  8689  mulge0  8692  recexap  8726  mulap0b  8728  lt2msq  8959  zaddcl  9412  zdiv  9461  zextlt  9465  prime  9472  uzind2  9485  fzind  9488  lbzbi  9737  xltneg  9958  xlt2add  10002  iocssre  10075  icossre  10076  iccssre  10077  fzen  10165  rebtwn2zlemshrink  10396  qbtwnxr  10400  ioo0  10402  ioom  10403  ico0  10404  ioc0  10405  expclzaplem  10708  expnegzap  10718  expaddzap  10728  expmulzap  10730  omgadd  10947  elovmpowrd  11035  shftuz  11128  cau3lem  11425  climuni  11604  efltim  12009  divalgb  12236  ndvdssub  12241  bitsfzo  12266  dvdsgcd  12333  lcmgcdlem  12399  qredeu  12419  isprm3  12440  prmdvdsexpr  12472  prmexpb  12473  fermltl  12556  coprimeprodsq  12580  pythagtrip  12606  pcpremul  12616  pcdvdsb  12643  pc2dvds  12653  4sqlem12  12725  4sqlem18  12731  ctinf  12801  mulgaddcom  13482  ghmrn  13593  dvdsunit  13874  unitmulclb  13876  lmodvsdi  14073  lss0cl  14131  cnntr  14697  cncnp2m  14703  cnptoprest  14711  lmtopcnp  14722  cnmptcom  14770  hmeof1o  14781  blpnf  14872  blssps  14899  blss  14900  blssec  14910  neibl  14963  climcncf  15056  cnplimcim  15139  plyadd  15223  plymul  15224  bj-peano4  15891  triap  15968