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  1924  ax11  2107  ordelinel  4507  reusv6OLD  4561  onint  4602  ordsuc  4621  tfindsg  4667  findsg  4699  issref  5072  sotri2  5088  sotri3  5089  somincom  5096  fnun  5366  fvmpti  5617  zfrep6  5764  ovigg  5984  ndmovg  6019  tfrlem9  6417  tfr3  6431  omlimcl  6592  oneo  6595  nnneo  6665  pssnn  7097  inficl  7194  dfac2  7773  axdc2lem  8090  axextnd  8229  canthp1lem2  8291  gchinf  8295  inatsk  8416  indpi  8547  ltaddpr2  8675  reclem2pr  8688  supsrlem  8749  axrrecex  8801  zeo  10113  nn0ind-raph  10128  fzind2  10939  bcpasc  11349  bitsfzo  12642  bezoutlem1  12733  algcvgblem  12763  qredeq  12801  prmreclem2  12980  ramtcl2  13074  divsfval  13465  gsumval3  15207  pgpfac1lem3a  15327  fiinopn  16663  restntr  16928  lly1stc  17238  dgradd2  19665  dgrcolem2  19671  asinneg  20198  ftalem2  20327  ftalem4  20329  ftalem5  20330  bpos1lem  20537  rngoueqz  21113  h1de2ctlem  22150  pjclem4a  22794  pj3lem1  22802  chrelat2i  22961  sumdmdii  23011  elim2if  23168  axextdist  24227  funtransport  24726  areacirc  25034  mappow  25192  intvconlem1  25806  tartarmap  25991  iscol3  26197  isibg1a6  26228  isdmn3  26802  iotavalb  27733  wlkdvspthlem  28365  fargshiftf1  28382  bnj1468  29194  bnj517  29233  exdistrfNEW7  29482  lkrlspeqN  29983  hlrelat2  30214  ps-1  30288  dalem54  30537  cdleme42c  31283  dihmeetlem6  32121
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