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 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used 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  5674  poxp  6472  fvn0elsuppb  6496  suppfnss  6501  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  nndi  6763  nnmass  6764  pr2nelem  7544  xnn0lenn0nn0  10285  difelfzle  10559  fzo1fzo0n0  10613  elfzo0z  10614  fzofzim  10618  elfzodifsumelfzo  10637  mulexp  11037  expadd  11040  expmul  11043  bernneq  11120  facdiv  11199  pfxfv  11479  swrdswrdlem  11499  pfxccat3  11529  reuccatpfxs1lem  11541  dvdsaddre2b  12634  addmodlteqALT  12652  ltoddhalfle  12686  halfleoddlt  12687  dfgcd2  12817  cncongr1  12907  oddprmgt2  12939  prmfac1  12957  infpnlem1  13168  dfgrp3me  13965  mulgaddcom  14009  mulginvcom  14010  assamulgscm  15153  fiinopn  15242  opnneissb  15393  blssps  15665  blss  15666  bcmono  16316  gausslemma2dlem1a  16394  2sqlem10  16461  ausgrumgrien  16628  ausgrusgrien  16629  ushgredgedg  16684  ushgredgedgloop  16686  edg0usgr  16705  0uhgrsubgr  16723  subumgredg2en  16729  wlkl1loop  16816  clwwlkccatlem  16858  umgrclwwlkge2  16860  clwwlkn1loopb  16878  clwwlkext2edg  16880  clwwlknonex2lem2  16896  clwwlknonex2  16897  clwwlknonex2e  16898  eupth2lem3lem6fi  16929