Theorem 3imp 1220

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

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

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 1007

This theorem is referenced by:  3impa  1221  3imp31  1223  3imp231  1224  3impb  1226  3impia  1227  3impib  1228  3com23  1236  3an1rs  1246  3imp1  1247  3impd  1248  syl3an2  1308  syl3an3  1309  3jao  1338  biimp3ar  1383  f1ssf1  5648  poxp  6430  fvn0elsuppb  6454  suppfnss  6459  tfrlemibxssdm  6560  tfr1onlembxssdm  6576  tfrcllembxssdm  6589  nndi  6721  nnmass  6722  pr2nelem  7490  xnn0lenn0nn0  10204  difelfzle  10475  fzo1fzo0n0  10529  elfzo0z  10530  fzofzim  10534  elfzodifsumelfzo  10553  mulexp  10947  expadd  10950  expmul  10953  bernneq  11030  facdiv  11108  pfxfv  11384  swrdswrdlem  11404  pfxccat3  11434  reuccatpfxs1lem  11446  dvdsaddre2b  12535  addmodlteqALT  12553  ltoddhalfle  12587  halfleoddlt  12588  dfgcd2  12718  cncongr1  12808  oddprmgt2  12839  prmfac1  12857  infpnlem1  13065  dfgrp3me  13834  mulgaddcom  13884  mulginvcom  13885  fiinopn  14918  opnneissb  15069  blssps  15341  blss  15342  gausslemma2dlem1a  15980  2sqlem10  16047  ausgrumgrien  16214  ausgrusgrien  16215  ushgredgedg  16270  ushgredgedgloop  16272  edg0usgr  16291  0uhgrsubgr  16309  subumgredg2en  16315  wlkl1loop  16402  clwwlkccatlem  16444  umgrclwwlkge2  16446  clwwlkn1loopb  16464  clwwlkext2edg  16466  clwwlknonex2lem2  16482  clwwlknonex2  16483  clwwlknonex2e  16484  eupth2lem3lem6fi  16515