Theorem 3expia 1207

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expia	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1204	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 124	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

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  7273  ltbtwnnqq  7501  prarloclem4  7584  addlocpr  7622  1idprl  7676  1idpru  7677  ltexprlemrnd  7691  recexprlemrnd  7715  recexprlem1ssl  7719  recexprlem1ssu  7720  recexprlemss1l  7721  recexprlemss1u  7722  aptisr  7865  axpre-apti  7971  ltxrlt  8111  axapti  8116  lttri3  8125  reapti  8625  apreap  8633  msqge0  8662  mulge0  8665  recexap  8699  mulap0b  8701  lt2msq  8932  zaddcl  9385  zdiv  9433  zextlt  9437  prime  9444  uzind2  9457  fzind  9460  lbzbi  9709  xltneg  9930  xlt2add  9974  iocssre  10047  icossre  10048  iccssre  10049  fzen  10137  rebtwn2zlemshrink  10362  qbtwnxr  10366  ioo0  10368  ioom  10369  ico0  10370  ioc0  10371  expclzaplem  10674  expnegzap  10684  expaddzap  10694  expmulzap  10696  omgadd  10913  elovmpowrd  10995  shftuz  11001  cau3lem  11298  climuni  11477  efltim  11882  divalgb  12109  ndvdssub  12114  bitsfzo  12139  dvdsgcd  12206  lcmgcdlem  12272  qredeu  12292  isprm3  12313  prmdvdsexpr  12345  prmexpb  12346  fermltl  12429  coprimeprodsq  12453  pythagtrip  12479  pcpremul  12489  pcdvdsb  12516  pc2dvds  12526  4sqlem12  12598  4sqlem18  12604  ctinf  12674  mulgaddcom  13354  ghmrn  13465  dvdsunit  13746  unitmulclb  13748  lmodvsdi  13945  lss0cl  14003  cnntr  14569  cncnp2m  14575  cnptoprest  14583  lmtopcnp  14594  cnmptcom  14642  hmeof1o  14653  blpnf  14744  blssps  14771  blss  14772  blssec  14782  neibl  14835  climcncf  14928  cnplimcim  15011  plyadd  15095  plymul  15096  bj-peano4  15709  triap  15786