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

Theorem syl3an3 1217
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 1150 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl7 63 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ta ) ) )
543imp 1145 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl3an3b  1220  syl3an3br  1223  vtoclgft  2834  disji  4011  ovmpt2x  5976  ovmpt2ga  5977  unbnn2  7114  axdc3lem4  8079  axdclem2  8147  gruiin  8432  gruen  8434  divass  9442  ltmul2  9607  xleadd1  10575  xltadd2  10577  xlemul1  10610  xltmul2  10613  elfzo  10877  modcyc2  11000  faclbnd5  11311  subcn2  12068  mulcn2  12069  ndvdsp1  12608  gcddiv  12728  lubel  14226  oddvdsi  14863  odcong  14864  odeq  14865  efgsp1  15046  lspsnss  15747  iuncld  16782  neips  16850  opnneip  16856  hmeof1o2  17454  ordthmeo  17493  ufinffr  17624  elfm3  17645  blcntr  17964  neibl  18047  blnei  18048  metss  18054  stdbdmetval  18060  prdsms  18077  lmmbr  18684  lmmbr2  18685  iscau2  18703  bcthlem1  18746  bcthlem3  18748  bcthlem4  18749  dvn2bss  19279  dvfsumrlim  19378  dvfsumrlim2  19379  cxpexpz  20014  cxpsub  20029  gxpval  20926  gxnn0neg  20930  gxnn0suc  20931  gxcl  20932  gxneg  20933  gxcom  20936  gxinv  20937  gxsuc  20939  gxnn0add  20941  gxadd  20942  gxsub  20943  gxnn0mul  20944  gxmul  20945  hvaddsub12  21617  hvaddsubass  21620  hvsubdistr1  21628  hvsubcan  21653  hhssnv  21841  spanunsni  22158  homco1  22381  homulass  22382  hoadddir  22384  hosubdi  22388  hoaddsubass  22395  hosubsub4  22398  lnopmi  22580  adjlnop  22666  mdsymlem5  22987  disjif  23355  disjif2  23358  sigaclfu  23480  wfrlem14  24269  sndw2  25101  tartarmap  25888  clsint2  26247  comppfsc  26307  isbnd2  26507  blbnd  26511  isdrngo2  26589  jm2.22  27088  jm2.23  27089  lindsmm2  27299  dvconstbi  27551  eelT11  28483  eelT12  28486  eelTT1  28488  eelT01  28489  eel0T1  28490  bnj544  28926  bnj561  28935  bnj562  28936  bnj594  28944  atnem0  29508  hlrelat5N  29590  ltrnel  30328  ltrnat  30329  ltrncnvat  30330
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator