Theorem syl5bir 184

Description: A mixed syllogism inference.

Hypotheses

Ref	Expression
syl5bir.1	|- (ph -> (ps <-> ch))
syl5bir.2	|- (th -> ch)

Assertion

Ref	Expression
syl5bir	|- (ph -> (th -> ps))

Proof of Theorem syl5bir

Step	Hyp	Ref	Expression
1		syl5bir.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimprd 136	. 2 |- (ph -> (ch -> ps))
3		syl5bir.2	. 2 |- (th -> ch)
4	2, 3	syl5 22	1 |- (ph -> (th -> ps))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  hbsb4t 906  reuhyp 1581  unineq 1680  elsnc2g 1831  ssopab2 2119  sotrieq 2149  supsn 2168  fr2nr 2177  fr3nr 2178  tz7.2 2183  ordtri1 2231  ordtri3 2234  onunit 2250  oneqmin 2273  limelon 2286  nlimsuc 2363  ordzsl 2366  limom 2387  findsg 2398  tfindsg 2402  vtoclrbr 2450  ralxp 2456  funcnvuni 2706  fco 2760  ndmfv 2848  fvco 2865  fsn 2895  funfvima 2904  isomin 2937  isofrlem 2939  tfrlem1 2949  tfrlem10 2958  tfrlem11 2959  ndmoprcl 3058  oacl 3138  omcl 3139  oecl 3140  oa0r 3141  om0r 3142  om1r 3145  oe1m 3147  oaordi 3148  oawordri 3152  oaass 3163  omordi 3164  nnacl 3172  nnmcl 3173  nnacom 3175  nndi 3180  nnmass 3181  nnmsucr 3182  nnmcom 3183  nnmord 3189  omsmolem 3195  brecop 3242  eceqopreq 3249  th3qlem1 3250  f1oeng 3298  f1domg 3299  fundmen 3333  unen 3338  pw2en 3348  mapxpen 3390  xpmapenlem4 3394  php 3409  pssnn 3428  suc11reg 3456  inf3lemd 3463  inf3lem1 3464  inf3lem3 3466  r1tr 3498  tz9.12lem1 3503  rankr1 3518  aceq5 3563  aceq6a 3564  kmlem8 3587  numthlem 3598  zornlem1 3603  alephon 3671  alephordlem2 3678  alephordi 3679  alephsucdom 3685  alephle 3689  isinfcard 3692  cflim 3704  addnidpi 3822  indpi 3828  addcmpblnq 3846  mulcmpblnq 3847  genpprecl 3898  genpnmax 3904  distrlem5pr 3925  prlem934b 3932  addcmpblnr 3975  recexsrlem 4006  map2psrpr 4014  axmulgt0 4086  addcan 4120  mulcan 4207  ltnet 4282  ltlet 4286  nnmulclt 4437  nnleltp1t 4448  nnsub 4450  crulem 4528  nn0subt 4587  zaddclt 4590  zltp1let 4597  uzind 4603  qret 4631  om2uzuz 4653  seqrn 4673  0expt 4680  1expt 4681  expaddt 4698  nneo 4719  sqrlem18 4748  sqrge0 4760  sqr2irr 4782  ruclem13 4897  infxpidmlem10 4942  infxpidmlem11 4943  his6 5057  orthcom 5061  ocsh 5164  ocin 5177  projlem8 5200  projlem13 5205  pjthlem11 5235  shsvat 5285  hsupss 5310  shslej 5339  shsidm 5358  shmods 5363  chnlen0 5369  h1de2b 5459  h1de2ctlem 5460  h1de2ct 5461  h1datom 5483  osumlem1 5530  3oalem1 5552  pjrn 5587  pjclem4 5653  pj3s 5659  ssmd1 5734  atcveq0 5746  atom1d 5750  chcv1t 5751  atcvat4 5775

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org