Theorem 3imp 1198

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

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

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 985

This theorem is referenced by:  3impa  1199  3imp31  1201  3imp231  1202  3impb  1204  3impia  1205  3impib  1206  3com23  1214  3an1rs  1224  3imp1  1225  3impd  1226  syl3an2  1286  syl3an3  1287  3jao  1316  biimp3ar  1361  poxp  6348  tfrlemibxssdm  6443  tfr1onlembxssdm  6459  tfrcllembxssdm  6472  nndi  6602  nnmass  6603  pr2nelem  7332  xnn0lenn0nn0  10029  difelfzle  10298  fzo1fzo0n0  10351  elfzo0z  10352  fzofzim  10356  elfzodifsumelfzo  10374  mulexp  10767  expadd  10770  expmul  10773  bernneq  10849  facdiv  10927  pfxfv  11182  swrdswrdlem  11202  pfxccat3  11232  reuccatpfxs1lem  11244  dvdsaddre2b  12318  addmodlteqALT  12336  ltoddhalfle  12370  halfleoddlt  12371  dfgcd2  12501  cncongr1  12591  oddprmgt2  12622  prmfac1  12640  infpnlem1  12848  dfgrp3me  13599  mulgaddcom  13649  mulginvcom  13650  fiinopn  14643  opnneissb  14794  blssps  15066  blss  15067  gausslemma2dlem1a  15702  2sqlem10  15769  ausgrumgrien  15933  ausgrusgrien  15934  ushgredgedg  15989  ushgredgedgloop  15991