Theorem 3imp 1217

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

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

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 1004

This theorem is referenced by:  3impa  1218  3imp31  1220  3imp231  1221  3impb  1223  3impia  1224  3impib  1225  3com23  1233  3an1rs  1243  3imp1  1244  3impd  1245  syl3an2  1305  syl3an3  1306  3jao  1335  biimp3ar  1380  poxp  6389  tfrlemibxssdm  6484  tfr1onlembxssdm  6500  tfrcllembxssdm  6513  nndi  6645  nnmass  6646  pr2nelem  7380  xnn0lenn0nn0  10078  difelfzle  10347  fzo1fzo0n0  10400  elfzo0z  10401  fzofzim  10405  elfzodifsumelfzo  10424  mulexp  10817  expadd  10820  expmul  10823  bernneq  10899  facdiv  10977  pfxfv  11237  swrdswrdlem  11257  pfxccat3  11287  reuccatpfxs1lem  11299  dvdsaddre2b  12373  addmodlteqALT  12391  ltoddhalfle  12425  halfleoddlt  12426  dfgcd2  12556  cncongr1  12646  oddprmgt2  12677  prmfac1  12695  infpnlem1  12903  dfgrp3me  13654  mulgaddcom  13704  mulginvcom  13705  fiinopn  14699  opnneissb  14850  blssps  15122  blss  15123  gausslemma2dlem1a  15758  2sqlem10  15825  ausgrumgrien  15989  ausgrusgrien  15990  ushgredgedg  16045  ushgredgedgloop  16047  edg0usgr  16066  wlkl1loop  16130  clwwlkccatlem  16169  umgrclwwlkge2  16171  clwwlkn1loopb  16188  clwwlkext2edg  16190