Theorem 3imp 1220

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

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

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 1007

This theorem is referenced by:  3impa  1221  3imp31  1223  3imp231  1224  3impb  1226  3impia  1227  3impib  1228  3com23  1236  3an1rs  1246  3imp1  1247  3impd  1248  syl3an2  1308  syl3an3  1309  3jao  1338  biimp3ar  1383  f1ssf1  5624  poxp  6406  fvn0elsuppb  6430  suppfnss  6435  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  nndi  6697  nnmass  6698  pr2nelem  7439  xnn0lenn0nn0  10143  difelfzle  10412  fzo1fzo0n0  10466  elfzo0z  10467  fzofzim  10471  elfzodifsumelfzo  10490  mulexp  10884  expadd  10887  expmul  10890  bernneq  10966  facdiv  11044  pfxfv  11312  swrdswrdlem  11332  pfxccat3  11362  reuccatpfxs1lem  11374  dvdsaddre2b  12463  addmodlteqALT  12481  ltoddhalfle  12515  halfleoddlt  12516  dfgcd2  12646  cncongr1  12736  oddprmgt2  12767  prmfac1  12785  infpnlem1  12993  dfgrp3me  13744  mulgaddcom  13794  mulginvcom  13795  fiinopn  14795  opnneissb  14946  blssps  15218  blss  15219  gausslemma2dlem1a  15857  2sqlem10  15924  ausgrumgrien  16091  ausgrusgrien  16092  ushgredgedg  16147  ushgredgedgloop  16149  edg0usgr  16168  0uhgrsubgr  16186  subumgredg2en  16192  wlkl1loop  16279  clwwlkccatlem  16321  umgrclwwlkge2  16323  clwwlkn1loopb  16341  clwwlkext2edg  16343  clwwlknonex2lem2  16359  clwwlknonex2  16360  clwwlknonex2e  16361  eupth2lem3lem6fi  16392