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  5645  poxp  6427  fvn0elsuppb  6451  suppfnss  6456  tfrlemibxssdm  6557  tfr1onlembxssdm  6573  tfrcllembxssdm  6586  nndi  6718  nnmass  6719  pr2nelem  7487  xnn0lenn0nn0  10194  difelfzle  10464  fzo1fzo0n0  10518  elfzo0z  10519  fzofzim  10523  elfzodifsumelfzo  10542  mulexp  10936  expadd  10939  expmul  10942  bernneq  11018  facdiv  11096  pfxfv  11369  swrdswrdlem  11389  pfxccat3  11419  reuccatpfxs1lem  11431  dvdsaddre2b  12520  addmodlteqALT  12538  ltoddhalfle  12572  halfleoddlt  12573  dfgcd2  12703  cncongr1  12793  oddprmgt2  12824  prmfac1  12842  infpnlem1  13050  dfgrp3me  13802  mulgaddcom  13852  mulginvcom  13853  fiinopn  14856  opnneissb  15007  blssps  15279  blss  15280  gausslemma2dlem1a  15918  2sqlem10  15985  ausgrumgrien  16152  ausgrusgrien  16153  ushgredgedg  16208  ushgredgedgloop  16210  edg0usgr  16229  0uhgrsubgr  16247  subumgredg2en  16253  wlkl1loop  16340  clwwlkccatlem  16382  umgrclwwlkge2  16384  clwwlkn1loopb  16402  clwwlkext2edg  16404  clwwlknonex2lem2  16420  clwwlknonex2  16421  clwwlknonex2e  16422  eupth2lem3lem6fi  16453