Theorem 3imp 1193

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  3impa  1194  3imp31  1196  3imp231  1197  3impb  1199  3impia  1200  3impib  1201  3com23  1209  3an1rs  1219  3imp1  1220  3impd  1221  syl3an2  1272  syl3an3  1273  3jao  1301  biimp3ar  1346  poxp  6233  tfrlemibxssdm  6328  tfr1onlembxssdm  6344  tfrcllembxssdm  6357  nndi  6487  nnmass  6488  pr2nelem  7190  xnn0lenn0nn0  9865  difelfzle  10134  fzo1fzo0n0  10183  elfzo0z  10184  fzofzim  10188  elfzodifsumelfzo  10201  mulexp  10559  expadd  10562  expmul  10565  bernneq  10641  facdiv  10718  dvdsaddre2b  11848  addmodlteqALT  11865  ltoddhalfle  11898  halfleoddlt  11899  dfgcd2  12015  cncongr1  12103  oddprmgt2  12134  prmfac1  12152  infpnlem1  12357  dfgrp3me  12970  mulgaddcom  13007  mulginvcom  13008  fiinopn  13507  opnneissb  13658  blssps  13930  blss  13931  2sqlem10  14475