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

Step	Hyp	Ref	Expression
1		syl5bir.1	. . 3 |- (ph -> (ps <-> ch))
2		syl5bir.2	. . 3 |- (th -> ch)
3	1, 2	syl5bir 210	. 2 |- (ph -> (th -> ps))
4	3	com12 11	1 |- (th -> (ph -> ps))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  elsnc2g 2436  reuhyp 2905  fr2nr 2925  fr3nr 2926  tz7.2 2931  ordtri1 2980  oneqmin 3018  nlimsucg 3112  opelxpex2 3279  funcnvuni 3564  fsn 3834  fconst2g 3845  funfvima 3852  ndmoprcl 4044  omordi 4197  omord 4199  omwordi 4202  omsmolem 4256  pw2en 4446  php 4513  pwfiOLD 4571  suppr 4590  suc11reg 4605  inf3lemd 4612  tz9.12lem1 4659  aceq5 4740  isinfcard 4887  addnidpi 5028  distrlem5pr 5131  cnegext 5348  xrmax1 5909  xrmin2 5912  max1ALT 5916  nnleltp1t 5954  sup2 6051  xrsupexmnf 6074  xrinfmexpnf 6075  xrub 6080  nnnn0addclt 6125  nn0subt 6161  zltp1let 6181  qret 6259  elfzp1 6510  fz1sbct 6517  fsequb 6523  expp1t 6574  expge0t 6591  sqrlem18 6690  seq1bnd 6910  reccnv 7218  infcvgaux1 7219  expcnv 7233  elcncf1d 7270  infxpidmlem10 7561  nvmul0or 8272  ipasslem5 8494  ipasslem11 8500  minveclem10 8554  efifolem5 8726  circgrp 8740  hvmul0ort 8894  his6t 8965  ocsh 9156  ocin 9169  projlem8 9193  shslej 9338  shsidm 9357  chnlen0 9368  h1de2b 9477  h1de2ctlem 9478  h1de2ct 9479  osumlem1 9578  3oalem1 9607  atcveq0 10275  chcv1t 10282  cdjreu 10359  cdj3lem2b 10364  homcard 10539  eqindhome 10541  filintf 10569  trran 10636

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