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  1338  3gencl  2805  moi  2955  ifnebibdc  3614  sotricim  4369  elirr  4588  en2lp  4601  suc11g  4604  3optocl  4752  sefvex  5596  f1oresrab  5744  ovmpos  6068  ov2gf  6069  poxp  6317  brtposg  6339  dfsmo2  6372  smoiun  6386  tfrlemibxssdm  6412  tfr1onlemsucfn  6425  tfr1onlemsucaccv  6426  tfr1onlembxssdm  6428  tfr1onlembfn  6429  tfr1onlemaccex  6433  tfr1onlemres  6434  tfrcllemsucfn  6438  tfrcllemsucaccv  6439  tfrcllembxssdm  6441  tfrcllembfn  6442  tfrcllemaccex  6446  tfrcllemres  6447  tfrcl  6449  nnsucsssuc  6577  nnaordi  6593  nnawordex  6614  mapvalg  6744  pmvalg  6745  elmapg  6747  xpdom3m  6928  ordiso  7137  ctssdc  7214  pr2ne  7299  ltbtwnnqq  7527  prarloclem4  7610  addlocpr  7648  1idprl  7702  1idpru  7703  ltexprlemrnd  7717  recexprlemrnd  7741  recexprlem1ssl  7745  recexprlem1ssu  7746  recexprlemss1l  7747  recexprlemss1u  7748  aptisr  7891  axpre-apti  7997  ltxrlt  8137  axapti  8142  lttri3  8151  reapti  8651  apreap  8659  msqge0  8688  mulge0  8691  recexap  8725  mulap0b  8727  lt2msq  8958  zaddcl  9411  zdiv  9460  zextlt  9464  prime  9471  uzind2  9484  fzind  9487  lbzbi  9736  xltneg  9957  xlt2add  10001  iocssre  10074  icossre  10075  iccssre  10076  fzen  10164  rebtwn2zlemshrink  10394  qbtwnxr  10398  ioo0  10400  ioom  10401  ico0  10402  ioc0  10403  expclzaplem  10706  expnegzap  10716  expaddzap  10726  expmulzap  10728  omgadd  10945  elovmpowrd  11033  shftuz  11070  cau3lem  11367  climuni  11546  efltim  11951  divalgb  12178  ndvdssub  12183  bitsfzo  12208  dvdsgcd  12275  lcmgcdlem  12341  qredeu  12361  isprm3  12382  prmdvdsexpr  12414  prmexpb  12415  fermltl  12498  coprimeprodsq  12522  pythagtrip  12548  pcpremul  12558  pcdvdsb  12585  pc2dvds  12595  4sqlem12  12667  4sqlem18  12673  ctinf  12743  mulgaddcom  13424  ghmrn  13535  dvdsunit  13816  unitmulclb  13818  lmodvsdi  14015  lss0cl  14073  cnntr  14639  cncnp2m  14645  cnptoprest  14653  lmtopcnp  14664  cnmptcom  14712  hmeof1o  14723  blpnf  14814  blssps  14841  blss  14842  blssec  14852  neibl  14905  climcncf  14998  cnplimcim  15081  plyadd  15165  plymul  15166  bj-peano4  15824  triap  15901