Theorem 3imp 1156

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 945	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3imp.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 254	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	sylbi 120	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 943

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

This theorem depends on definitions:  df-bi 116  df-3an 945

This theorem is referenced by:  3impa  1157  3impb  1158  3impia  1159  3impib  1160  3com23  1168  3an1rs  1178  3imp1  1179  3impd  1180  syl3an2  1231  syl3an3  1232  3jao  1260  biimp3ar  1305  poxp  6081  tfrlemibxssdm  6176  tfr1onlembxssdm  6192  tfrcllembxssdm  6205  nndi  6334  nnmass  6335  pr2nelem  6994  xnn0lenn0nn0  9535  difelfzle  9798  fzo1fzo0n0  9847  elfzo0z  9848  fzofzim  9852  elfzodifsumelfzo  9865  mulexp  10219  expadd  10222  expmul  10225  bernneq  10299  facdiv  10371  addmodlteqALT  11399  ltoddhalfle  11432  halfleoddlt  11433  dfgcd2  11542  cncongr1  11624  oddprmgt2  11654  prmfac1  11670  fiinopn  12008  opnneissb  12161  blssps  12410  blss  12411