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 2440  reuhyp 2911  fr2nr 2931  fr3nr 2932  tz7.2 2937  ordtri1 2986  oneqmin 3024  nlimsucg 3118  opelxpex2 3285  funcnvuni 3570  fsn 3840  fconst2g 3851  funfvima 3858  ndmoprcl 4050  omordi 4203  omord 4205  omwordi 4208  omsmolem 4262  pw2en 4452  php 4519  pwfi 4579  pwfiOLD 4580  suppr 4599  suc11reg 4614  inf3lemd 4621  tz9.12lem1 4669  aceq5 4750  isinfcard 4898  addnidpi 5040  distrlem5pr 5143  cnegext 5360  xrmax1 5911  xrmin2 5914  max1ALT 5918  nnleltp1t 5956  sup2 6053  xrsupexmnf 6076  xrinfmexpnf 6077  xrub 6082  nnnn0addclt 6127  nn0subt 6163  zltp1let 6183  qret 6260  elfzp1 6511  fz1sbct 6518  fsequb 6524  expp1t 6575  expge0t 6592  sqrlem18 6691  seq1bnd 6910  reccnv 7218  infcvgaux1 7219  expcnv 7233  elcncf1d 7270  infxpidmlem10 7562  nvmul0or 8268  ipasslem5 8490  ipasslem11 8496  minveclem10 8550  efifolem5 8721  circgrp 8735  hvmul0ort 8889  his6t 8960  ocsh 9151  ocin 9164  projlem8 9188  shslej 9333  shsidm 9352  chnlen0 9363  h1de2b 9472  h1de2ctlem 9473  h1de2ct 9474  osumlem1 9573  3oalem1 9602  atcveq0 10270  chcv1t 10277  cdjreu 10354  cdj3lem2b 10359  homcard 10525  eqindhome 10527  filintf 10554  trran 10607

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