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

Theorem syl3an3 1170
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 1158 . 2 ((𝜓𝜒𝜑) → (𝜓𝜒𝜃))
3 syl3an3.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 17 1 ((𝜓𝜒𝜑) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  3adant3l  1194  3adant3r  1196  syl3an3b  1512  syl3an3br  1515  vtoclgftOLD  3391  disji  4785  ovmpt2x  6950  ovmpt2ga  6951  wfrlem14  7593  unbnn2  8378  axdc3lem4  9463  axdclem2  9530  gruiin  9820  gruen  9822  divass  10891  ltmul2  11062  xleadd1  12274  xltadd2  12276  xlemul1  12309  xltmul2  12312  elfzo  12662  modcyc2  12896  faclbnd5  13275  relexprel  13974  subcn2  14520  mulcn2  14521  ndvdsp1  15333  gcddiv  15466  lcmneg  15514  lubel  17319  gsumccatsn  17577  mulgaddcom  17761  oddvdsi  18163  odcong  18164  odeq  18165  efgsp1  18346  lspsnss  19188  lindsmm2  20366  mulmarep1el  20576  mdetunilem4  20619  iuncld  21047  neips  21115  opnneip  21121  comppfsc  21533  hmeof1o2  21764  ordthmeo  21803  ufinffr  21930  elfm3  21951  utop3cls  22252  blcntrps  22414  blcntr  22415  neibl  22503  blnei  22504  metss  22510  stdbdmetval  22516  prdsms  22533  blval2  22564  lmmbr  23252  lmmbr2  23253  iscau2  23271  bcthlem1  23317  bcthlem3  23319  bcthlem4  23320  dvn2bss  23888  dvfsumrlim  23989  dvfsumrlim2  23990  cxpexpz  24608  cxpsub  24623  relogbzexp  24709  upgr4cycl4dv4e  27333  konigsbergssiedgwpr  27397  dlwwlknondlwlknonf1o  27522  hvaddsub12  28200  hvaddsubass  28203  hvsubdistr1  28211  hvsubcan  28236  hhssnv  28426  spanunsni  28743  homco1  28965  homulass  28966  hoadddir  28968  hosubdi  28972  hoaddsubass  28979  hosubsub4  28982  lnopmi  29164  adjlnop  29250  mdsymlem5  29571  disjif  29694  disjif2  29697  ind0  30385  sigaclfu  30487  bnj544  31267  bnj561  31276  bnj562  31277  bnj594  31285  clsint2  32626  ftc1anclem6  33799  isbnd2  33891  blbnd  33895  isdrngo2  34066  atnem0  35104  hlrelat5N  35186  ltrnel  35924  ltrnat  35925  ltrncnvat  35926  jm2.22  38060  jm2.23  38061  dvconstbi  39031  eelT11  39430  eelT12  39432  eelTT1  39433  eelT01  39434  eel0T1  39435  liminfvalxr  40514  rmfsupp  42661  mndpfsupp  42663  scmfsupp  42665  dignn0flhalflem2  42916
  Copyright terms: Public domain W3C validator