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

Theorem syl3an3 1263
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an3.1  |-  ( ph  ->  th )
syl3an3.2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
Assertion
Ref Expression
syl3an3  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )

Proof of Theorem syl3an3
StepHypRef Expression
1 syl3an3.1 . . 3  |-  ( ph  ->  th )
2 syl3an3.2 . . . 4  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
323exp 1195 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl7 68 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ta ) ) )
543imp 1190 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  syl3an3b  1266  syl3an3br  1269  vtoclgft  3161  disji  4435  ovmpt2x  6416  ovmpt2ga  6417  unbnn2  7778  axdc3lem4  8834  axdclem2  8901  gruiin  9189  gruen  9191  divass  10226  ltmul2  10394  xleadd1  11448  xltadd2  11450  xlemul1  11483  xltmul2  11486  elfzo  11800  modcyc2  12001  faclbnd5  12345  subcn2  13383  mulcn2  13384  ndvdsp1  13929  gcddiv  14049  lubel  15612  gsumccatsn  15846  oddvdsi  16387  odcong  16388  odeq  16389  efgsp1  16570  lspsnss  17448  lindsmm2  18671  mulmarep1el  18881  mdetunilem4  18924  iuncld  19352  neips  19420  opnneip  19426  comppfsc  19860  hmeof1o2  20091  ordthmeo  20130  ufinffr  20257  elfm3  20278  utop3cls  20581  blcntrps  20742  blcntr  20743  neibl  20831  blnei  20832  metss  20838  stdbdmetval  20844  prdsms  20861  blval2  20905  lmmbr  21524  lmmbr2  21525  iscau2  21543  bcthlem1  21590  bcthlem3  21592  bcthlem4  21593  dvn2bss  22160  dvfsumrlim  22259  dvfsumrlim2  22260  cxpexpz  22873  cxpsub  22888  wlkcompim  24299  2pthon  24377  wwlknext  24497  wwlkextproplem3  24516  clwlkcompim  24537  clwwlkel  24566  clwwlkf  24567  numclwlk1lem2f1  24868  gxpval  25034  gxnn0neg  25038  gxnn0suc  25039  gxcl  25040  gxneg  25041  gxcom  25044  gxinv  25045  gxsuc  25047  gxnn0add  25049  gxadd  25050  gxsub  25051  gxnn0mul  25052  gxmul  25053  hvaddsub12  25728  hvaddsubass  25731  hvsubdistr1  25739  hvsubcan  25764  hhssnv  25953  spanunsni  26270  homco1  26493  homulass  26494  hoadddir  26496  hosubdi  26500  hoaddsubass  26507  hosubsub4  26510  lnopmi  26692  adjlnop  26778  mdsymlem5  27099  disjif  27209  disjif2  27212  ind0  27784  sigaclfu  27870  wfrlem14  29209  ftc1anclem6  29948  clsint2  30000  isbnd2  30109  blbnd  30113  isdrngo2  30191  jm2.22  30768  jm2.23  30769  lcmneg  31036  dvconstbi  31066  rmfsupp  32265  mndpfsupp  32267  scmfsupp  32269  eelT11  32793  eelT12  32797  eelTT1  32799  eelT01  32800  eel0T1  32801  bnj544  33248  bnj561  33257  bnj562  33258  bnj594  33266  atnem0  34332  hlrelat5N  34414  ltrnel  35152  ltrnat  35153  ltrncnvat  35154
  Copyright terms: Public domain W3C validator