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  6232  tfrlemibxssdm  6327  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  nndi  6486  nnmass  6487  pr2nelem  7189  xnn0lenn0nn0  9864  difelfzle  10133  fzo1fzo0n0  10182  elfzo0z  10183  fzofzim  10187  elfzodifsumelfzo  10200  mulexp  10558  expadd  10561  expmul  10564  bernneq  10640  facdiv  10717  dvdsaddre2b  11847  addmodlteqALT  11864  ltoddhalfle  11897  halfleoddlt  11898  dfgcd2  12014  cncongr1  12102  oddprmgt2  12133  prmfac1  12151  infpnlem1  12356  dfgrp3me  12969  mulgaddcom  13005  mulginvcom  13006  fiinopn  13474  opnneissb  13625  blssps  13897  blss  13898  2sqlem10  14442