Theorem 3imp 1196

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

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

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 983

This theorem is referenced by:  3impa  1197  3imp31  1199  3imp231  1200  3impb  1202  3impia  1203  3impib  1204  3com23  1212  3an1rs  1222  3imp1  1223  3impd  1224  syl3an2  1284  syl3an3  1285  3jao  1314  biimp3ar  1359  poxp  6325  tfrlemibxssdm  6420  tfr1onlembxssdm  6436  tfrcllembxssdm  6449  nndi  6579  nnmass  6580  pr2nelem  7306  xnn0lenn0nn0  9994  difelfzle  10263  fzo1fzo0n0  10314  elfzo0z  10315  fzofzim  10319  elfzodifsumelfzo  10337  mulexp  10730  expadd  10733  expmul  10736  bernneq  10812  facdiv  10890  pfxfv  11143  swrdswrdlem  11163  dvdsaddre2b  12196  addmodlteqALT  12214  ltoddhalfle  12248  halfleoddlt  12249  dfgcd2  12379  cncongr1  12469  oddprmgt2  12500  prmfac1  12518  infpnlem1  12726  dfgrp3me  13476  mulgaddcom  13526  mulginvcom  13527  fiinopn  14520  opnneissb  14671  blssps  14943  blss  14944  gausslemma2dlem1a  15579  2sqlem10  15646