HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem syl5cbir 211
Description: A mixed syllogism inference.
Hypotheses
Ref Expression
syl5bir.1 |- (ph -> (ps <-> ch))
syl5bir.2 |- (th -> ch)
Assertion
Ref Expression
syl5cbir |- (th -> (ph -> ps))
Proof of Theorem syl5cbir
StepHypRef Expression
1 syl5bir.1 . . 3 |- (ph -> (ps <-> ch))
2 syl5bir.2 . . 3 |- (th -> ch)
31, 2syl5bir 210 . 2 |- (ph -> (th -> ps))
43com12 11 1 |- (th -> (ph -> ps))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146
This theorem is referenced by:  elsnc2g 2426  reuhyp 2895  fr2nr 2915  fr3nr 2916  tz7.2 2921  ordtri1 2970  oneqmin 3008  nlimsucg 3102  funcnvuni 3550  fsn 3819  fconst2g 3830  funfvima 3837  ndmoprcl 4030  omordi 4181  omord 4183  omwordi 4186  omsmolem 4240  pw2en 4426  php 4493  pwfi 4545  suppr 4562  suc11reg 4577  inf3lemd 4584  tz9.12lem1 4631  aceq5 4712  isinfcard 4859  addnidpi 5000  distrlem5pr 5103  cnegext 5320  xrmax1 5857  xrmin2 5860  max1ALT 5864  nnleltp1t 5901  sup2 5998  xrsupexmnf 6021  xrinfmexpnf 6022  xrub 6027  nnnn0addclt 6072  nn0subt 6108  zltp1let 6128  qret 6197  elfzp1 6442  fz1sbct 6449  fsequb 6455  expp1t 6506  expge0t 6522  sqrlem18 6620  seq1bnd 6847  reccnv 7153  infcvgaux1 7154  expcnv 7168  elcncf1d 7205  infxpidmlem10 7504  nvmul0or 8212  ipasslem5 8425  ipasslem11 8431  minveclem10 8485  efifolem5 8641  circgrp 8660  hvmul0ort 8815  his6t 8886  ocsh 9072  ocin 9085  projlem8 9109  shslej 9253  shsidm 9272  chnlen0 9283  h1de2b 9392  h1de2bOLD 9393  h1de2ctlem 9394  h1de2ct 9395  osumlem1 9495  3oalem1 9524  atcveq0 10183  chcv1t 10190  cdjreu 10264  cdj3lem2b 10269  homcard 10426  filintf 10443  trran 10480
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147
Copyright terms: Public domain