Theorem 3imp 1195

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

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

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 982

This theorem is referenced by:  3impa  1196  3imp31  1198  3imp231  1199  3impb  1201  3impia  1202  3impib  1203  3com23  1211  3an1rs  1221  3imp1  1222  3impd  1223  syl3an2  1283  syl3an3  1284  3jao  1312  biimp3ar  1357  poxp  6299  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  nndi  6553  nnmass  6554  pr2nelem  7272  xnn0lenn0nn0  9959  difelfzle  10228  fzo1fzo0n0  10278  elfzo0z  10279  fzofzim  10283  elfzodifsumelfzo  10296  mulexp  10689  expadd  10692  expmul  10695  bernneq  10771  facdiv  10849  dvdsaddre2b  12025  addmodlteqALT  12043  ltoddhalfle  12077  halfleoddlt  12078  dfgcd2  12208  cncongr1  12298  oddprmgt2  12329  prmfac1  12347  infpnlem1  12555  dfgrp3me  13304  mulgaddcom  13354  mulginvcom  13355  fiinopn  14348  opnneissb  14499  blssps  14771  blss  14772  gausslemma2dlem1a  15407  2sqlem10  15474