Theorem 3imp 1175

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

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

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 964

This theorem is referenced by:  3impa  1176  3impb  1177  3impia  1178  3impib  1179  3com23  1187  3an1rs  1197  3imp1  1198  3impd  1199  syl3an2  1250  syl3an3  1251  3jao  1279  biimp3ar  1324  poxp  6129  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  nndi  6382  nnmass  6383  pr2nelem  7047  xnn0lenn0nn0  9648  difelfzle  9911  fzo1fzo0n0  9960  elfzo0z  9961  fzofzim  9965  elfzodifsumelfzo  9978  mulexp  10332  expadd  10335  expmul  10338  bernneq  10412  facdiv  10484  addmodlteqALT  11557  ltoddhalfle  11590  halfleoddlt  11591  dfgcd2  11702  cncongr1  11784  oddprmgt2  11814  prmfac1  11830  fiinopn  12171  opnneissb  12324  blssps  12596  blss  12597