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 1244  pm2.61ne 1625  unineq 2245  ssopab2 2811  sotrieq 2852  alxfr 2886  eldifpw 2900  ordtri3 2973  ssonunit 2984  limelon 3022  ordzsl 3106  limom 3136  findsg 3147  tfindsg 3152  vtoclrbr 3202  ralxp 3208  fco 3621  ndmfv 3730  fvco 3759  isomin 3884  isofrlem 3886  tfrlem1 3896  tfrlem11 3906  oacl 4154  omcl 4155  oecl 4156  oa0r 4157  om0r 4158  om1r 4161  oe1m 4163  oaordi 4164  oawordri 4168  oaass 4179  omwordri 4187  odi 4194  omass 4195  oewordri 4203  oeworde 4204  oeordsuc 4205  oelim2 4206  nnacl 4213  nnmcl 4214  nnecl 4215  nnacom 4217  nnmsucr 4224  nnmcom 4225  brecop 4290  eceqopreq 4297  th3qlem1 4298  f1oen2g 4375  f1domg 4377  fundmen 4409  unen 4414  mapxpen 4475  xpmapenlem4 4479  php 4493  pssnn 4513  domfi 4516  supsnALT 4564  inf3lem1 4585  inf3lem3 4587  noinfep 4612  r1tr 4626  rankr1 4646  aceq6a 4713  kmlem9 4745  numthlem 4755  zorn2lem1 4760  alephon 4837  alephordlem2 4845  alephordi 4846  alephsucdom 4852  alephle 4856  alephfplem3 4870  cflim 4881  indpi 5006  addcmpblnq 5024  mulcmpblnq 5025  genpprecl 5076  genpnmax 5082  prlem934b 5110  addcmpblnr 5153  recexsrlem 5184  map2psrpr 5192  pre-axmulgt0 5262  cnegextlem1 5317  addcan 5323  ltnet 5488  ltnetOLD 5489  ltlet 5493  xrltlet 5532  mulcan 5659  nnmulclt 5889  nnsub 5903  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxrunb1 6036  supxrunb2 6037  nn0subt 6108  zaddclt 6112  zltp1let 6128  nneo 6144  uzindOLD 6156  om2uzuz 6234  seq1rn2 6258  elioc2t 6322  elico2t 6323  elicc2t 6324  uz11t 6364  elfzlem 6405  fzoptht 6434  seqzrn2 6488  1expt 6516  expaddt 6527  expmult 6528  sqrge0 6632  sqr2irr 6659  crulem 6666  nn0absclt 6816  recant 6842  faclbnd 6882  bccl2t 6909  fsum1s2 6948  climcmplem 7073  isumclt 7144  efcltlem2 7247  abspef01tlub 7336  ruclem13 7465  infxpidmlem11 7505  tgss2t 7579  cncnplem4 7716  blf 7784  lmsslem 7887  xplm 7909  xpcn 7910  cmsss 7931  grplactf1o 8034  nmosetre 8359  nmobndseqi 8372  orthcom 8895  hhcms 8993  hhsscms 9067  projlem13 9114  pjthlem11 9144  shsvat 9199  hsupss 9224  shmods 9277  h1datom 9421  pjrn 9564  nmopsetretALT 9707  nmfnsetret 9721  lnopcnbdt 9880  pjclem4 10037  pj3s 10045  ssmd1 10146  atom1d 10188  chjatom 10192  atcvat4 10232  cdj3lem2a 10268  cdj3lem3a 10271  findreccl 10324  inpws1 10351  mapudiscn 10399  efilcp2 10450  iint 10478

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