Theorem 3imp 1224

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

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

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 1011

This theorem is referenced by:  3impa  1225  3imp31  1227  3imp231  1228  3impb  1230  3impia  1231  3impib  1232  3com23  1240  3an1rs  1250  3imp1  1251  3impd  1252  syl3an2  1312  syl3an3  1313  3jao  1342  biimp3ar  1387  f1ssf1  5669  poxp  6462  fvn0elsuppb  6486  suppfnss  6491  tfrlemibxssdm  6592  tfr1onlembxssdm  6608  tfrcllembxssdm  6621  nndi  6753  nnmass  6754  pr2nelem  7531  xnn0lenn0nn0  10250  difelfzle  10524  fzo1fzo0n0  10578  elfzo0z  10579  fzofzim  10583  elfzodifsumelfzo  10602  mulexp  10998  expadd  11001  expmul  11004  bernneq  11081  facdiv  11159  pfxfv  11439  swrdswrdlem  11459  pfxccat3  11489  reuccatpfxs1lem  11501  dvdsaddre2b  12591  addmodlteqALT  12609  ltoddhalfle  12643  halfleoddlt  12644  dfgcd2  12774  cncongr1  12864  oddprmgt2  12895  prmfac1  12913  infpnlem1  13121  dfgrp3me  13888  mulgaddcom  13932  mulginvcom  13933  assamulgscm  15026  fiinopn  15088  opnneissb  15239  blssps  15511  blss  15512  gausslemma2dlem1a  16160  2sqlem10  16227  ausgrumgrien  16394  ausgrusgrien  16395  ushgredgedg  16450  ushgredgedgloop  16452  edg0usgr  16471  0uhgrsubgr  16489  subumgredg2en  16495  wlkl1loop  16582  clwwlkccatlem  16624  umgrclwwlkge2  16626  clwwlkn1loopb  16644  clwwlkext2edg  16646  clwwlknonex2lem2  16662  clwwlknonex2  16663  clwwlknonex2e  16664  eupth2lem3lem6fi  16695