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  6384  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  nndi  6640  nnmass  6641  pr2nelem  7372  xnn0lenn0nn0  10069  difelfzle  10338  fzo1fzo0n0  10391  elfzo0z  10392  fzofzim  10396  elfzodifsumelfzo  10415  mulexp  10808  expadd  10811  expmul  10814  bernneq  10890  facdiv  10968  pfxfv  11224  swrdswrdlem  11244  pfxccat3  11274  reuccatpfxs1lem  11286  dvdsaddre2b  12360  addmodlteqALT  12378  ltoddhalfle  12412  halfleoddlt  12413  dfgcd2  12543  cncongr1  12633  oddprmgt2  12664  prmfac1  12682  infpnlem1  12890  dfgrp3me  13641  mulgaddcom  13691  mulginvcom  13692  fiinopn  14686  opnneissb  14837  blssps  15109  blss  15110  gausslemma2dlem1a  15745  2sqlem10  15812  ausgrumgrien  15976  ausgrusgrien  15977  ushgredgedg  16032  ushgredgedgloop  16034  wlkl1loop  16079