Theorem syl3an3 1183

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)

Hypotheses

Ref	Expression
syl3an3.1	⊢ (𝜑 → 𝜃)
syl3an3.2	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3an3	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Proof of Theorem syl3an3

Step	Hyp	Ref	Expression
1		syl3an3.1	. . 3 ⊢ (𝜑 → 𝜃)
2	1	3anim3i 1172	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an3.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 18	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant3l  1199  3adant3r  1200  syl3an3b  1432  syl3an3br  1435  disji  5096  ovmpox  7569  ovmpoga  7570  wrecseq123  8312  dif1en  9149  domtrfil  9179  ssdomfi2  9184  domnsymfi  9187  sdomdomtrfi  9188  domsdomtrfi  9189  phplem2  9192  php  9194  php3  9196  findcard3  9246  unbnn2  9260  axdc3lem4  10448  axdclem2  10515  gruiin  10806  gruen  10808  divass  11901  ltmul2  12077  ind0  12239  xleadd1  13292  xltadd2  13294  xlemul1  13327  xltmul2  13330  elfzo  13701  modcyc2  13953  faclbnd5  14347  swrdrevpfx  14823  relexprel  15095  subcn2  15665  mulcn2  15666  ndvdsp1  16486  gcddiv  16626  lcmneg  16678  lubel  18587  mndpfsupp  18848  gsumccatsn  18925  mulgaddcom  19187  oddvdsi  19641  odcong  19642  odeq  19643  efgsp1  19830  lspsnss  21140  rnglidlrng  21410  lindsmm2  22008  mulmarep1el  22758  mdetunilem4  22801  iuncld  23231  neips  23299  opnneip  23305  comppfsc  23718  hmeof1o2  23949  ordthmeo  23988  ufinffr  24115  elfm3  24136  utop3cls  24437  blcntrps  24598  blcntr  24599  neibl  24687  blnei  24688  metss  24694  stdbdmetval  24700  prdsms  24717  blval2  24748  lmmbr  25446  lmmbr2  25447  iscau2  25465  bcthlem1  25512  bcthlem3  25514  bcthlem4  25515  dvn2bss  26118  dvfsumrlim  26219  dvfsumrlim2  26220  cxpexpz  26861  cxpsub  26876  cxpcom  26933  relogbzexp  26970  ltsubs1  28298  1ewlk  30495  1pthon2ve  30534  upgr4cycl4dv4e  30565  konigsbergssiedgwpr  30629  dlwwlknondlwlknonf1o  30745  hvaddsub12  31419  hvaddsubass  31422  hvsubdistr1  31430  hvsubcan  31455  hhssnv  31645  spanunsni  31960  homco1  32182  homulass  32183  hoadddir  32185  hosubdi  32189  hoaddsubass  32196  hosubsub4  32199  lnopmi  32381  adjlnop  32467  mdsymlem5  32788  disjif  32952  disjif2  32955  sigaclfu  34532  signstfvc  34985  bnj544  35306  bnj561  35315  bnj562  35316  bnj594  35324  fineqvnttrclselem3  35552  satfvsuc  35866  satfvsucsuc  35870  clsint2  36873  weiunso  37010  weiunwe  37013  ftc1anclem6  38382  isbnd2  38467  blbnd  38471  isdrngo2  38642  atnem0  40125  hlrelat5N  40208  ltrnel  40946  ltrnat  40947  ltrncnvat  40948  nnproddivdvdsd  42800  dvdsexpnn  43127  jm2.22  43755  jm2.23  43756  dvconstbi  45077  eelT11  45448  eelT12  45450  eelTT1  45451  eelT01  45452  eel0T1  45453  liminfvalxr  46530  grlimprclnbgr  48794  rmfsupp  49186  scmfsupp  49188  dignn0flhalflem2  49429  rrx2vlinest  49554  rrx2linesl  49556