MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3an3 Structured version   Visualization version   GIF version

Theorem syl3an3 1161
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
StepHypRef Expression
1 syl3an3.1 . . 3 (𝜑𝜃)
213anim3i 1150 . 2 ((𝜓𝜒𝜑) → (𝜓𝜒𝜃))
3 syl3an3.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 17 1 ((𝜓𝜒𝜑) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  3adant3l  1176  3adant3r  1177  syl3an3b  1401  syl3an3br  1404  disji  5048  ovmpox  7302  ovmpoga  7303  wfrlem14  7967  unbnn2  8774  axdc3lem4  9874  axdclem2  9941  gruiin  10231  gruen  10233  divass  11315  ltmul2  11490  xleadd1  12647  xltadd2  12649  xlemul1  12682  xltmul2  12685  elfzo  13039  modcyc2  13274  faclbnd5  13657  relexprel  14397  subcn2  14950  mulcn2  14951  ndvdsp1  15761  gcddiv  15898  lcmneg  15946  lubel  17731  gsumccatsn  18007  mulgaddcom  18250  oddvdsi  18675  odcong  18676  odeq  18677  efgsp1  18862  lspsnss  19761  lindsmm2  20972  mulmarep1el  21180  mdetunilem4  21223  iuncld  21652  neips  21720  opnneip  21726  comppfsc  22139  hmeof1o2  22370  ordthmeo  22409  ufinffr  22536  elfm3  22557  utop3cls  22859  blcntrps  23021  blcntr  23022  neibl  23110  blnei  23111  metss  23117  stdbdmetval  23123  prdsms  23140  blval2  23171  lmmbr  23860  lmmbr2  23861  iscau2  23879  bcthlem1  23926  bcthlem3  23928  bcthlem4  23929  dvn2bss  24526  dvfsumrlim  24627  dvfsumrlim2  24628  cxpexpz  25249  cxpsub  25264  cxpcom  25319  relogbzexp  25353  1ewlk  27893  1pthon2ve  27932  upgr4cycl4dv4e  27963  konigsbergssiedgwpr  28027  dlwwlknondlwlknonf1o  28143  hvaddsub12  28814  hvaddsubass  28817  hvsubdistr1  28825  hvsubcan  28850  hhssnv  29040  spanunsni  29355  homco1  29577  homulass  29578  hoadddir  29580  hosubdi  29584  hoaddsubass  29591  hosubsub4  29594  lnopmi  29776  adjlnop  29862  mdsymlem5  30183  disjif  30327  disjif2  30330  ind0  31277  sigaclfu  31378  signstfvc  31844  bnj544  32166  bnj561  32175  bnj562  32176  bnj594  32184  swrdrevpfx  32363  satfvsuc  32608  satfvsucsuc  32612  clsint2  33677  ftc1anclem6  34971  isbnd2  35060  blbnd  35064  isdrngo2  35235  atnem0  36453  hlrelat5N  36536  ltrnel  37274  ltrnat  37275  ltrncnvat  37276  jm2.22  39592  jm2.23  39593  dvconstbi  40666  eelT11  41041  eelT12  41043  eelTT1  41044  eelT01  41045  eel0T1  41046  liminfvalxr  42064  rmfsupp  44423  mndpfsupp  44425  scmfsupp  44427  dignn0flhalflem2  44677  rrx2vlinest  44729  rrx2linesl  44731
  Copyright terms: Public domain W3C validator