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

Theorem syl6bir 222
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 216 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6bir.2 . 2  |-  ( ch 
->  th )
42, 3syl6 32 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  19.21t  1814  exdistrfOLD  2068  ax11  2234  tppreqb  3941  ordelinel  4682  reusv6OLD  4736  onint  4777  ordsuc  4796  tfindsg  4842  findsg  4874  issref  5249  sotri2  5265  sotri3  5266  somincom  5273  fnun  5553  fvmpti  5807  zfrep6  5970  ovigg  6196  ndmovg  6232  tfrlem9  6648  tfr3  6662  omlimcl  6823  oneo  6826  nnneo  6896  pssnn  7329  inficl  7432  dfac2  8013  axdc2lem  8330  axextnd  8468  canthp1lem2  8530  gchinf  8534  inatsk  8655  indpi  8786  ltaddpr2  8914  reclem2pr  8927  supsrlem  8988  axrrecex  9040  zeo  10357  nn0ind-raph  10372  fzind2  11200  bcpasc  11614  bitsfzo  12949  bezoutlem1  13040  algcvgblem  13070  qredeq  13108  prmreclem2  13287  ramtcl2  13381  divsfval  13774  gsumval3  15516  pgpfac1lem3a  15636  fiinopn  16976  restntr  17248  lly1stc  17561  dgradd2  20188  dgrcolem2  20194  asinneg  20728  ftalem2  20858  ftalem4  20860  ftalem5  20861  bpos1lem  21068  wlkdvspthlem  21609  fargshiftf1  21626  hashnbgravdg  21684  rngoueqz  22020  h1de2ctlem  23059  pjclem4a  23703  pj3lem1  23711  chrelat2i  23870  sumdmdii  23920  elim2if  24007  axextdist  25429  funtransport  25967  areacirc  26299  isdmn3  26686  iotavalb  27609  cusgraisrusgra  28379  bnj1468  29219  bnj517  29258  exdistrfNEW7  29507  lkrlspeqN  29971  hlrelat2  30202  ps-1  30276  dalem54  30525  cdleme42c  31271  dihmeetlem6  32109
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 179
  Copyright terms: Public domain W3C validator