Theorem 3expia 1229

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

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 1004

This theorem is referenced by:  ad5ant125  1265  mp3an3  1360  3gencl  2834  moi  2986  ifnebibdc  3648  sotricim  4414  elirr  4633  en2lp  4646  suc11g  4649  3optocl  4797  sefvex  5650  f1oresrab  5802  ovmpos  6134  ov2gf  6135  poxp  6384  brtposg  6406  dfsmo2  6439  smoiun  6453  tfrlemibxssdm  6479  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemaccex  6513  tfrcllemres  6514  tfrcl  6516  nnsucsssuc  6646  nnaordi  6662  nnawordex  6683  mapvalg  6813  pmvalg  6814  elmapg  6816  xpdom3m  7001  ordiso  7214  ctssdc  7291  pr2ne  7376  ltbtwnnqq  7613  prarloclem4  7696  addlocpr  7734  1idprl  7788  1idpru  7789  ltexprlemrnd  7803  recexprlemrnd  7827  recexprlem1ssl  7831  recexprlem1ssu  7832  recexprlemss1l  7833  recexprlemss1u  7834  aptisr  7977  axpre-apti  8083  ltxrlt  8223  axapti  8228  lttri3  8237  reapti  8737  apreap  8745  msqge0  8774  mulge0  8777  recexap  8811  mulap0b  8813  lt2msq  9044  zaddcl  9497  zdiv  9546  zextlt  9550  prime  9557  uzind2  9570  fzind  9573  lbzbi  9823  xltneg  10044  xlt2add  10088  iocssre  10161  icossre  10162  iccssre  10163  fzen  10251  rebtwn2zlemshrink  10485  qbtwnxr  10489  ioo0  10491  ioom  10492  ico0  10493  ioc0  10494  expclzaplem  10797  expnegzap  10807  expaddzap  10817  expmulzap  10819  omgadd  11036  elovmpowrd  11126  ccatopth2  11264  pfxccatin12  11280  shftuz  11343  cau3lem  11640  climuni  11819  efltim  12224  divalgb  12451  ndvdssub  12456  bitsfzo  12481  dvdsgcd  12548  lcmgcdlem  12614  qredeu  12634  isprm3  12655  prmdvdsexpr  12687  prmexpb  12688  fermltl  12771  coprimeprodsq  12795  pythagtrip  12821  pcpremul  12831  pcdvdsb  12858  pc2dvds  12868  4sqlem12  12940  4sqlem18  12946  ctinf  13016  mulgaddcom  13698  ghmrn  13809  dvdsunit  14091  unitmulclb  14093  lmodvsdi  14290  lss0cl  14348  cnntr  14914  cncnp2m  14920  cnptoprest  14928  lmtopcnp  14939  cnmptcom  14987  hmeof1o  14998  blpnf  15089  blssps  15116  blss  15117  blssec  15127  neibl  15180  climcncf  15273  cnplimcim  15356  plyadd  15440  plymul  15441  upgredg2vtx  15961  bj-peano4  16373  triap  16457