Theorem 3expia 1236

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 1233	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 124	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ad5ant125  1272  mp3an3  1367  3gencl  2856  moi  3009  ifnebibdc  3686  sotricim  4470  elirr  4690  en2lp  4703  suc11g  4706  3optocl  4855  sefvex  5719  f1oresrab  5876  ovmpos  6215  ov2gf  6216  poxp  6472  brtposg  6529  dfsmo2  6562  smoiun  6576  tfrlemibxssdm  6602  tfr1onlemsucfn  6615  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllemsucfn  6628  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemaccex  6636  tfrcllemres  6637  tfrcl  6639  nnsucsssuc  6769  nnaordi  6785  nnawordex  6806  mapvalg  6936  pmvalg  6937  elmapg  6939  xpdom3m  7136  ordiso  7382  ctssdc  7459  pr2ne  7544  ltbtwnnqq  7788  prarloclem4  7871  addlocpr  7909  1idprl  7963  1idpru  7964  ltexprlemrnd  7978  recexprlemrnd  8002  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  aptisr  8152  axpre-apti  8258  ltxrlt  8397  axapti  8402  lttri3  8411  reapti  8915  apreap  8923  msqge0  8952  mulge0  8955  recexap  8989  mulap0b  8991  lt2msq  9224  zaddcl  9695  zdiv  9745  zextlt  9749  prime  9756  uzind2  9769  fzind  9772  lbzbi  10032  xltneg  10255  xlt2add  10299  iocssre  10372  icossre  10373  iccssre  10374  fzen  10464  rebtwn2zlemshrink  10705  qbtwnxr  10709  ioo0  10711  ioom  10712  ico0  10713  ioc0  10714  expclzaplem  11021  expnegzap  11031  expaddzap  11041  expmulzap  11043  omgadd  11264  elovmpowrd  11368  ccatopth2  11511  pfxccatin12  11527  shftuz  11604  cau3lem  11903  climuni  12084  efltim  12490  divalgb  12717  ndvdssub  12722  bitsfzo  12747  dvdsgcd  12814  lcmgcdlem  12880  qredeu  12900  isprm3  12921  prmdvdsexpr  12954  prmexpb  12955  fermltl  13041  coprimeprodsq  13065  pythagtrip  13091  pcpremul  13101  pcdvdsb  13128  pc2dvds  13138  4sqlem12  13210  4sqlem18  13216  ballotfilemirc  13333  ctinf  13379  mulgaddcom  14008  ghmrn  14119  gsumcom2fi  14275  dvdsunit  14528  unitmulclb  14530  lmodvsdi  14757  lss0cl  14815  cnntr  15451  cncnp2m  15457  cnptoprest  15465  lmtopcnp  15476  cnmptcom  15524  hmeof1o  15535  blpnf  15626  blssps  15653  blss  15654  blssec  15664  neibl  15717  climcncf  15810  cnplimcim  15893  plyadd  15977  plymul  15978  rpcxpmul2z  16148  chtublem  16295  bposlem3  16313  upgredg2vtx  16594  lealltlt2  16957  dichmul0or  16965  bj-peano4  17186  triap  17284