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  5651  poxp  6441  fvn0elsuppb  6465  suppfnss  6470  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  nndi  6732  nnmass  6733  pr2nelem  7501  xnn0lenn0nn0  10220  difelfzle  10493  fzo1fzo0n0  10547  elfzo0z  10548  fzofzim  10552  elfzodifsumelfzo  10571  mulexp  10967  expadd  10970  expmul  10973  bernneq  11050  facdiv  11128  pfxfv  11404  swrdswrdlem  11424  pfxccat3  11454  reuccatpfxs1lem  11466  dvdsaddre2b  12555  addmodlteqALT  12573  ltoddhalfle  12607  halfleoddlt  12608  dfgcd2  12738  cncongr1  12828  oddprmgt2  12859  prmfac1  12877  infpnlem1  13085  dfgrp3me  13858  mulgaddcom  13902  mulginvcom  13903  fiinopn  14998  opnneissb  15149  blssps  15421  blss  15422  gausslemma2dlem1a  16060  2sqlem10  16127  ausgrumgrien  16294  ausgrusgrien  16295  ushgredgedg  16350  ushgredgedgloop  16352  edg0usgr  16371  0uhgrsubgr  16389  subumgredg2en  16395  wlkl1loop  16482  clwwlkccatlem  16524  umgrclwwlkge2  16526  clwwlkn1loopb  16544  clwwlkext2edg  16546  clwwlknonex2lem2  16562  clwwlknonex2  16563  clwwlknonex2e  16564  eupth2lem3lem6fi  16595