Theorem 3imp 1132

Description: Importation inference. (Contributed by NM, 8-Apr-1994.)

Hypothesis

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

Assertion

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

Proof of Theorem 3imp

Step	Hyp	Ref	Expression
1		df-3an 921	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3imp.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 252	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	sylbi 119	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

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

This theorem is referenced by:  3impa  1133  3impb  1134  3impia  1135  3impib  1136  3com23  1144  3an1rs  1150  3imp1  1151  3impd  1152  syl3an2  1203  syl3an3  1204  3jao  1232  biimp3ar  1277  poxp  5873  tfrlemibxssdm  5964  nndi  6088  nnmass  6089  pr2nelem  6460  difelfzle  9145  fzo1fzo0n0  9192  elfzo0z  9193  fzofzim  9197  elfzodifsumelfzo  9210  mulexp  9515  expadd  9518  expmul  9521  bernneq  9593  facdiv  9665  addmodlteqALT  10259  ltoddhalfle  10293  halfleoddlt  10294  dfgcd2  10403  cncongr1  10485  oddprmgt2  10515  prmfac1  10531