Theorem 3imp 1176

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

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

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

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

This theorem is referenced by:  3impa  1177  3imp31  1178  3imp231  1179  3impb  1181  3impia  1182  3impib  1183  3com23  1191  3an1rs  1201  3imp1  1202  3impd  1203  syl3an2  1254  syl3an3  1255  3jao  1283  biimp3ar  1328  poxp  6180  tfrlemibxssdm  6275  tfr1onlembxssdm  6291  tfrcllembxssdm  6304  nndi  6434  nnmass  6435  pr2nelem  7127  xnn0lenn0nn0  9770  difelfzle  10037  fzo1fzo0n0  10086  elfzo0z  10087  fzofzim  10091  elfzodifsumelfzo  10104  mulexp  10462  expadd  10465  expmul  10468  bernneq  10542  facdiv  10616  addmodlteqALT  11755  ltoddhalfle  11788  halfleoddlt  11789  dfgcd2  11902  cncongr1  11984  oddprmgt2  12015  prmfac1  12031  fiinopn  12444  opnneissb  12597  blssps  12869  blss  12870