Theorem 3expia 1140

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

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  mp3an3  1257  3gencl  2633  moi  2775  sotricim  4078  elirr  4284  en2lp  4297  suc11g  4300  3optocl  4436  sefvex  5216  f1oresrab  5350  ovmpt2s  5644  ov2gf  5645  poxp  5873  brtposg  5892  dfsmo2  5925  smoiun  5939  tfrlemibxssdm  5964  nnsucsssuc  6094  nnaordi  6104  nnawordex  6124  xpdom3m  6331  ordiso  6447  pr2ne  6461  ltbtwnnqq  6605  prarloclem4  6688  addlocpr  6726  1idprl  6780  1idpru  6781  ltexprlemrnd  6795  recexprlemrnd  6819  recexprlem1ssl  6823  recexprlem1ssu  6824  recexprlemss1l  6825  recexprlemss1u  6826  aptisr  6955  axpre-apti  7051  ltxrlt  7178  axapti  7183  lttri3  7191  reapti  7679  apreap  7687  msqge0  7716  mulge0  7719  recexap  7743  mulap0b  7745  lt2msq  7964  zaddcl  8391  zdiv  8435  zextlt  8439  prime  8446  uzind2  8459  fzind  8462  lbzbi  8701  xltneg  8903  iocssre  8976  icossre  8977  iccssre  8978  fzen  9062  qbtwnzlemshrink  9258  rebtwn2zlemshrink  9262  qbtwnxr  9266  ioo0  9268  ioom  9269  ico0  9270  ioc0  9271  expival  9478  expclzaplem  9500  expnegzap  9510  expaddzap  9520  expmulzap  9522  shftuz  9705  cau3lem  10000  climuni  10132  divalgb  10325  ndvdssub  10330  dvdsgcd  10401  lcmgcdlem  10459  qredeu  10479  isprm3  10500  prmdvdsexpr  10529  prmexpb  10530  bj-peano4  10750