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

Theorem syl3an3 1219
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 1152 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl7 65 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ta ) ) )
543imp 1147 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  syl3an3b  1222  syl3an3br  1225  vtoclgft  2946  disji  4142  ovmpt2x  6142  ovmpt2ga  6143  unbnn2  7301  axdc3lem4  8267  axdclem2  8334  gruiin  8619  gruen  8621  divass  9629  ltmul2  9794  xleadd1  10767  xltadd2  10769  xlemul1  10802  xltmul2  10805  elfzo  11073  modcyc2  11205  faclbnd5  11517  subcn2  12316  mulcn2  12317  ndvdsp1  12857  gcddiv  12977  lubel  14477  oddvdsi  15114  odcong  15115  odeq  15116  efgsp1  15297  lspsnss  15994  iuncld  17033  neips  17101  opnneip  17107  hmeof1o2  17717  ordthmeo  17756  ufinffr  17883  elfm3  17904  utop3cls  18203  blcntr  18339  neibl  18422  blnei  18423  metss  18429  stdbdmetval  18435  prdsms  18452  blval2  18483  lmmbr  19083  lmmbr2  19084  iscau2  19102  bcthlem1  19147  bcthlem3  19149  bcthlem4  19150  dvn2bss  19684  dvfsumrlim  19783  dvfsumrlim2  19784  cxpexpz  20426  cxpsub  20441  constr2pth  21450  2pthon  21451  gxpval  21696  gxnn0neg  21700  gxnn0suc  21701  gxcl  21702  gxneg  21703  gxcom  21706  gxinv  21707  gxsuc  21709  gxnn0add  21711  gxadd  21712  gxsub  21713  gxnn0mul  21714  gxmul  21715  hvaddsub12  22389  hvaddsubass  22392  hvsubdistr1  22400  hvsubcan  22425  hhssnv  22613  spanunsni  22930  homco1  23153  homulass  23154  hoadddir  23156  hosubdi  23160  hoaddsubass  23167  hosubsub4  23170  lnopmi  23352  adjlnop  23438  mdsymlem5  23759  disjif  23865  disjif2  23868  ind0  24214  sigaclfu  24299  wfrlem14  25294  clsint2  26024  comppfsc  26079  isbnd2  26184  blbnd  26188  isdrngo2  26266  jm2.22  26758  jm2.23  26759  lindsmm2  26969  dvconstbi  27221  eelT11  28153  eelT12  28157  eelTT1  28159  eelT01  28160  eel0T1  28161  bnj544  28604  bnj561  28613  bnj562  28614  bnj594  28622  atnem0  29434  hlrelat5N  29516  ltrnel  30254  ltrnat  30255  ltrncnvat  30256
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator