Theorem 3imp 1219

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

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

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 1006

This theorem is referenced by:  3impa  1220  3imp31  1222  3imp231  1223  3impb  1225  3impia  1226  3impib  1227  3com23  1235  3an1rs  1245  3imp1  1246  3impd  1247  syl3an2  1307  syl3an3  1308  3jao  1337  biimp3ar  1382  f1ssf1  5618  poxp  6402  tfrlemibxssdm  6498  tfr1onlembxssdm  6514  tfrcllembxssdm  6527  nndi  6659  nnmass  6660  pr2nelem  7401  xnn0lenn0nn0  10105  difelfzle  10374  fzo1fzo0n0  10428  elfzo0z  10429  fzofzim  10433  elfzodifsumelfzo  10452  mulexp  10846  expadd  10849  expmul  10852  bernneq  10928  facdiv  11006  pfxfv  11274  swrdswrdlem  11294  pfxccat3  11324  reuccatpfxs1lem  11336  dvdsaddre2b  12425  addmodlteqALT  12443  ltoddhalfle  12477  halfleoddlt  12478  dfgcd2  12608  cncongr1  12698  oddprmgt2  12729  prmfac1  12747  infpnlem1  12955  dfgrp3me  13706  mulgaddcom  13756  mulginvcom  13757  fiinopn  14757  opnneissb  14908  blssps  15180  blss  15181  gausslemma2dlem1a  15816  2sqlem10  15883  ausgrumgrien  16050  ausgrusgrien  16051  ushgredgedg  16106  ushgredgedgloop  16108  edg0usgr  16127  0uhgrsubgr  16145  subumgredg2en  16151  wlkl1loop  16238  clwwlkccatlem  16280  umgrclwwlkge2  16282  clwwlkn1loopb  16300  clwwlkext2edg  16302  clwwlknonex2lem2  16318  clwwlknonex2  16319  clwwlknonex2e  16320  eupth2lem3lem6fi  16351