Theorem syl3an3 1165

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 1154	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an3.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 17	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adant3l  1181  3adant3r  1182  syl3an3b  1407  syl3an3br  1410  disji  5104  ovmpox  7558  ovmpoga  7559  wrecseq123  8311  wfrlem14OLD  8334  dif1en  9172  dif1enOLD  9174  domtrfil  9204  ssdomfi2  9209  domnsymfi  9212  sdomdomtrfi  9213  domsdomtrfi  9214  phplem2  9217  php  9219  php3  9221  findcard3  9288  unbnn2  9303  axdc3lem4  10465  axdclem2  10532  gruiin  10822  gruen  10824  divass  11912  ltmul2  12090  xleadd1  13269  xltadd2  13271  xlemul1  13304  xltmul2  13307  elfzo  13676  modcyc2  13922  faclbnd5  14314  relexprel  15056  subcn2  15609  mulcn2  15610  ndvdsp1  16428  gcddiv  16568  lcmneg  16620  lubel  18522  mndpfsupp  18743  gsumccatsn  18819  mulgaddcom  19079  oddvdsi  19527  odcong  19528  odeq  19529  efgsp1  19716  lspsnss  20945  rnglidlrng  21206  lindsmm2  21787  mulmarep1el  22508  mdetunilem4  22551  iuncld  22981  neips  23049  opnneip  23055  comppfsc  23468  hmeof1o2  23699  ordthmeo  23738  ufinffr  23865  elfm3  23886  utop3cls  24188  blcntrps  24349  blcntr  24350  neibl  24438  blnei  24439  metss  24445  stdbdmetval  24451  prdsms  24468  blval2  24499  lmmbr  25208  lmmbr2  25209  iscau2  25227  bcthlem1  25274  bcthlem3  25276  bcthlem4  25277  dvn2bss  25882  dvfsumrlim  25988  dvfsumrlim2  25989  cxpexpz  26626  cxpsub  26641  cxpcom  26698  relogbzexp  26736  sltsub1  28023  1ewlk  30042  1pthon2ve  30081  upgr4cycl4dv4e  30112  konigsbergssiedgwpr  30176  dlwwlknondlwlknonf1o  30292  hvaddsub12  30965  hvaddsubass  30968  hvsubdistr1  30976  hvsubcan  31001  hhssnv  31191  spanunsni  31506  homco1  31728  homulass  31729  hoadddir  31731  hosubdi  31735  hoaddsubass  31742  hosubsub4  31745  lnopmi  31927  adjlnop  32013  mdsymlem5  32334  disjif  32505  disjif2  32508  ind0  32781  sigaclfu  34096  signstfvc  34552  bnj544  34871  bnj561  34880  bnj562  34881  bnj594  34889  swrdrevpfx  35085  satfvsuc  35329  satfvsucsuc  35333  clsint2  36293  weiunso  36430  weiunwe  36433  ftc1anclem6  37668  isbnd2  37753  blbnd  37757  isdrngo2  37928  atnem0  39282  hlrelat5N  39366  ltrnel  40104  ltrnat  40105  ltrncnvat  40106  nnproddivdvdsd  41959  dvdsexpnn  42329  jm2.22  42966  jm2.23  42967  dvconstbi  44306  eelT11  44679  eelT12  44681  eelTT1  44682  eelT01  44683  eel0T1  44684  liminfvalxr  45760  rmfsupp  48296  scmfsupp  48298  dignn0flhalflem2  48544  rrx2vlinest  48669  rrx2linesl  48671