Theorem syl5bir 210

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 154	. 2 |- (ph -> (ch -> ps))
3		syl5bir.2	. 2 |- (th -> ch)
4	2, 3	syl5 21	1 |- (ph -> (th -> ps))

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

This theorem is referenced by:  syl5cbir 211  hbsb4t 1249  pm2.61ne 1633  unineq 2255  ssopab2 2822  sotrieq 2861  alxfr 2896  eldifpw 2910  ordtri3 2983  ssonunit 2994  limelon 3032  ordzsl 3116  limom 3146  findsg 3157  tfindsg 3162  vtoclrbr 3212  ralxp 3218  fco 3636  ndmfv 3745  fvco 3774  isomin 3899  isofrlem 3901  tfrlem1 3911  tfrlem11 3921  oacl 4170  omcl 4171  oecl 4172  oa0r 4173  om0r 4174  om1r 4177  oe1m 4179  oaordi 4180  oawordri 4184  oaass 4195  omwordri 4203  odi 4210  omass 4211  oewordri 4219  oeworde 4220  oeordsuc 4221  oelim2 4222  nnacl 4229  nnmcl 4230  nnecl 4231  nnacom 4233  nnmsucr 4240  nnmcom 4241  brecop 4306  eceqopreq 4313  th3qlem1 4314  f1oen2g 4394  f1domg 4396  fundmen 4428  unen 4434  mapxpen 4495  xpmapenlem4 4499  php 4513  pssnn 4534  domfiOLD 4539  supsnALT 4592  inf3lem1 4613  inf3lem3 4615  noinfep 4640  r1tr 4654  rankr1 4674  aceq6a 4741  kmlem9 4773  numthlem 4783  zorn2lem1 4788  alephon 4865  alephordlem2 4873  alephordi 4874  alephsucdom 4880  alephle 4884  alephfplem3 4898  cflim 4909  indpi 5034  addcmpblnq 5052  mulcmpblnq 5053  genpprecl 5104  genpnmax 5110  prlem934b 5138  addcmpblnr 5181  recexsrlem 5212  map2psrpr 5220  pre-axmulgt0 5290  cnegextlem1 5345  addcan 5351  ltnet 5516  ltlet 5520  xrltlet 5559  mulcan 5686  mulcanOLD 5687  nnmulclt 5941  nnsub 5956  xrsupsslem 6076  xrinfmsslem 6077  xrub 6080  supxrunb1 6089  supxrunb2 6090  nn0subt 6161  zaddclt 6165  zltp1let 6181  nneo 6197  uzindOLD 6208  om2uzuz 6297  seq1rn2 6321  elioc2t 6390  elico2t 6391  elicc2t 6392  uz11t 6432  elfzlem 6473  fzoptht 6502  seqzrn2 6556  1expt 6584  expaddt 6596  expmult 6597  sqrge0 6702  sqr2irr 6729  crulem 6736  nn0absclt 6879  recant 6905  faclbnd 6945  bccl2t 6971  fsum1s2 7010  climcmplem 7137  isumclt 7209  efcltlem2 7305  abspef01tlub 7395  ruclem13 7522  infxpidmlem11 7562  tgss2t 7637  cncnplem4 7777  blf 7844  lmsslem 7952  xplm 7975  xpcn 7976  cmsss 7997  grplactf1o 8098  nmosetre 8427  nmobndseqi 8440  spwpr3OLD 8662  orthcom 8974  hhcms 9072  hhsscms 9150  projlem13 9198  pjthlem11 9229  shsvat 9284  hsupss 9309  shmods 9362  h1datom 9504  pjrn 9647  nmopsetretALT 9790  nmfnsetret 9804  lnopcnbdt 9965  pjclem4 10127  pj3s 10135  ssmd1 10238  atom1d 10280  chjatom 10284  atcvat4 10324  cdj3lem2a 10363  cdj3lem3a 10366  findreccl 10417  nndivlub 10422  inpws1 10455  mapudiscn 10512  efilcp2 10581  efilcp2OLD 10582  iint 10634

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