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

Theorem syl6bir 220
Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)
Hypotheses
Ref Expression
syl6bir.1  |-  ( ph  ->  ( ch  <->  ps )
)
syl6bir.2  |-  ( ch 
->  th )
Assertion
Ref Expression
syl6bir  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6bir
StepHypRef Expression
1 syl6bir.1 . . 3  |-  ( ph  ->  ( ch  <->  ps )
)
21biimprd 214 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6bir.2 . 2  |-  ( ch 
->  th )
42, 3syl6 29 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  exdistrf  1911  ax11  2094  ordelinel  4491  reusv6OLD  4545  onint  4586  ordsuc  4605  tfindsg  4651  findsg  4683  issref  5056  sotri2  5072  sotri3  5073  somincom  5080  fnun  5350  fvmpti  5601  zfrep6  5748  ovigg  5968  ndmovg  6003  tfrlem9  6401  tfr3  6415  omlimcl  6576  oneo  6579  nnneo  6649  pssnn  7081  inficl  7178  dfac2  7757  axdc2lem  8074  axextnd  8213  canthp1lem2  8275  gchinf  8279  inatsk  8400  indpi  8531  ltaddpr2  8659  reclem2pr  8672  supsrlem  8733  axrrecex  8785  zeo  10097  nn0ind-raph  10112  fzind2  10923  bcpasc  11333  bitsfzo  12626  bezoutlem1  12717  algcvgblem  12747  qredeq  12785  prmreclem2  12964  ramtcl2  13058  divsfval  13449  gsumval3  15191  pgpfac1lem3a  15311  fiinopn  16647  restntr  16912  lly1stc  17222  dgradd2  19649  dgrcolem2  19655  asinneg  20182  ftalem2  20311  ftalem4  20313  ftalem5  20314  bpos1lem  20521  rngoueqz  21097  h1de2ctlem  22134  pjclem4a  22778  pj3lem1  22786  chrelat2i  22945  sumdmdii  22995  elim2if  23152  axextdist  24156  funpartfun  24481  funtransport  24654  areacirc  24931  mappow  25089  intvconlem1  25703  tartarmap  25888  iscol3  26094  isibg1a6  26125  isdmn3  26699  iotavalb  27630  bnj1468  28878  bnj517  28917  lkrlspeqN  29361  hlrelat2  29592  ps-1  29666  dalem54  29915  cdleme42c  30661  dihmeetlem6  31499
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
  Copyright terms: Public domain W3C validator