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

Theorem syl3an3 1358
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an3.1 (𝜑𝜃)
syl3an3.2 ((𝜓𝜒𝜃) → 𝜏)
Assertion
Ref Expression
syl3an3 ((𝜓𝜒𝜑) → 𝜏)

Proof of Theorem syl3an3
StepHypRef Expression
1 syl3an3.1 . . 3 (𝜑𝜃)
2 syl3an3.2 . . . 4 ((𝜓𝜒𝜃) → 𝜏)
323exp 1261 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl7 74 . 2 (𝜓 → (𝜒 → (𝜑𝜏)))
543imp 1254 1 ((𝜓𝜒𝜑) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  syl3an3b  1361  syl3an3br  1364  vtoclgftOLD  3241  disji  4600  ovmpt2x  6742  ovmpt2ga  6743  wfrlem14  7373  unbnn2  8161  axdc3lem4  9219  axdclem2  9286  gruiin  9576  gruen  9578  divass  10647  ltmul2  10818  xleadd1  12028  xltadd2  12030  xlemul1  12063  xltmul2  12066  elfzo  12413  modcyc2  12646  faclbnd5  13025  relexprel  13713  subcn2  14259  mulcn2  14260  ndvdsp1  15059  gcddiv  15192  lcmneg  15240  lubel  17043  gsumccatsn  17301  mulgaddcom  17485  oddvdsi  17888  odcong  17889  odeq  17890  efgsp1  18071  lspsnss  18909  lindsmm2  20087  mulmarep1el  20297  mdetunilem4  20340  iuncld  20759  neips  20827  opnneip  20833  comppfsc  21245  hmeof1o2  21476  ordthmeo  21515  ufinffr  21643  elfm3  21664  utop3cls  21965  blcntrps  22127  blcntr  22128  neibl  22216  blnei  22217  metss  22223  stdbdmetval  22229  prdsms  22246  blval2  22277  lmmbr  22964  lmmbr2  22965  iscau2  22983  bcthlem1  23029  bcthlem3  23031  bcthlem4  23032  dvn2bss  23599  dvfsumrlim  23698  dvfsumrlim2  23699  cxpexpz  24313  cxpsub  24328  relogbzexp  24414  upgr4cycl4dv4e  26911  konigsbergssiedgwpr  26976  hvaddsub12  27741  hvaddsubass  27744  hvsubdistr1  27752  hvsubcan  27777  hhssnv  27967  spanunsni  28284  homco1  28506  homulass  28507  hoadddir  28509  hosubdi  28513  hoaddsubass  28520  hosubsub4  28523  lnopmi  28705  adjlnop  28791  mdsymlem5  29112  disjif  29233  disjif2  29236  ind0  29860  sigaclfu  29960  bnj544  30669  bnj561  30678  bnj562  30679  bnj594  30687  clsint2  31963  ftc1anclem6  33119  isbnd2  33211  blbnd  33215  isdrngo2  33386  atnem0  34082  hlrelat5N  34164  ltrnel  34902  ltrnat  34903  ltrncnvat  34904  jm2.22  37039  jm2.23  37040  dvconstbi  38012  eelT11  38411  eelT12  38413  eelTT1  38414  eelT01  38415  eel0T1  38416  rmfsupp  41440  mndpfsupp  41442  scmfsupp  41444  dignn0flhalflem2  41699
  Copyright terms: Public domain W3C validator