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  5671  poxp  6468  fvn0elsuppb  6492  suppfnss  6497  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  nndi  6759  nnmass  6760  pr2nelem  7537  xnn0lenn0nn0  10269  difelfzle  10543  fzo1fzo0n0  10597  elfzo0z  10598  fzofzim  10602  elfzodifsumelfzo  10621  mulexp  11017  expadd  11020  expmul  11023  bernneq  11100  facdiv  11178  pfxfv  11458  swrdswrdlem  11478  pfxccat3  11508  reuccatpfxs1lem  11520  dvdsaddre2b  12610  addmodlteqALT  12628  ltoddhalfle  12662  halfleoddlt  12663  dfgcd2  12793  cncongr1  12883  oddprmgt2  12914  prmfac1  12932  infpnlem1  13140  dfgrp3me  13907  mulgaddcom  13951  mulginvcom  13952  assamulgscm  15045  fiinopn  15107  opnneissb  15258  blssps  15530  blss  15531  bcmono  16124  gausslemma2dlem1a  16189  2sqlem10  16256  ausgrumgrien  16423  ausgrusgrien  16424  ushgredgedg  16479  ushgredgedgloop  16481  edg0usgr  16500  0uhgrsubgr  16518  subumgredg2en  16524  wlkl1loop  16611  clwwlkccatlem  16653  umgrclwwlkge2  16655  clwwlkn1loopb  16673  clwwlkext2edg  16675  clwwlknonex2lem2  16691  clwwlknonex2  16692  clwwlknonex2e  16693  eupth2lem3lem6fi  16724