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  5088  ovmpox  7571  ovmpoga  7572  wrecseq123  8324  tz7.48lem  8443  dif1en  9170  domtrfil  9200  ssdomfi2  9205  domnsymfi  9208  sdomdomtrfi  9209  domsdomtrfi  9210  phplem2  9213  php  9215  php3  9217  findcard3  9267  unbnn2  9282  axdc3lem4  10524  axdclem2  10591  gruiin  10888  gruen  10890  divass  11985  ltmul2  12161  ind0  12323  xleadd1  13378  xltadd2  13380  xlemul1  13413  xltmul2  13416  elfzo  13788  modcyc2  14040  faclbnd5  14435  swrdrevpfx  14911  relexprel  15185  subcn2  15755  mulcn2  15756  ndvdsp1  16574  gcddiv  16717  dvdsexpnn  16733  lcmneg  16771  lubel  18681  mndpfsupp  18954  gsumccatsn  19032  mulgaddcom  19301  oddvdsi  19755  odcong  19756  odeq  19757  efgsp1  19944  lspsnss  21258  rnglidlrng  21528  lindsmm2  22128  mulmarep1el  22880  mdetunilem4  22923  iuncld  23356  neips  23424  opnneip  23430  comppfsc  23844  hmeof1o2  24075  ordthmeo  24114  ufinffr  24241  elfm3  24262  utop3cls  24563  blcntrps  24724  blcntr  24725  neibl  24813  blnei  24814  metss  24820  stdbdmetval  24826  prdsms  24843  blval2  24874  lmmbr  25572  lmmbr2  25573  iscau2  25591  bcthlem1  25638  bcthlem3  25640  bcthlem4  25641  dvn2bss  26243  dvfsumrlim  26344  dvfsumrlim2  26345  cxpexpz  26988  cxpsub  27003  cxpcom  27060  relogbzexp  27097  ltsubs1  28455  1ewlk  30699  1pthon2ve  30748  upgr4cycl4dv4e  30779  konigsbergssiedgwpr  30843  dlwwlknondlwlknonf1o  30959  hvaddsub12  31633  hvaddsubass  31636  hvsubdistr1  31644  hvsubcan  31669  hhssnv  31859  spanunsni  32174  homco1  32396  homulass  32397  hoadddir  32399  hosubdi  32403  hoaddsubass  32410  hosubsub4  32413  lnopmi  32595  adjlnop  32681  mdsymlem5  33002  disjif  33165  disjif2  33168  sigaclfu  34744  signstfvc  35196  bnj544  35517  bnj561  35526  bnj562  35527  bnj594  35535  fineqvnttrclselem3  35774  satfvsuc  36105  satfvsucsuc  36109  clsint2  37097  weiunso  37234  weiunwe  37237  ftc1anclem6  38596  isbnd2  38697  blbnd  38701  isdrngo2  38872  atnem0  40355  hlrelat5N  40438  ltrnel  41176  ltrnat  41177  ltrncnvat  41178  nnproddivdvdsd  43030  jm2.22  43981  jm2.23  43982  dvconstbi  45303  eelT11  45674  eelT12  45676  eelTT1  45677  eelT01  45678  eel0T1  45679  liminfvalxr  46762  grlimprclnbgr  49063  rmfsupp  49454  scmfsupp  49456  dignn0flhalflem2  49697  rrx2vlinest  49822  rrx2linesl  49824