Theorem syl5bir 208

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

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

This theorem is referenced by:  syl5cbir 209  hbsb4t 1287  pm2.61ne 1679  unineq 2307  ssopab2 2900  sotrieq 2940  ordtri3 3011  limelon 3036  alxfr 3119  eldifpw 3133  ssonuni 3148  ordzsl 3199  tfindsg 3213  limom 3233  findsg 3245  vtoclrbr 3295  ralxp 3301  fco 3743  ndmfv 3856  fvco 3885  isomin 4013  isofrlem 4015  tfrlem1 4212  tfrlem11 4222  oacl 4306  omcl 4307  oecl 4308  oa0r 4309  om0r 4310  om1r 4313  oe1m 4315  oaordi 4316  oawordri 4320  oaass 4331  omwordri 4339  odi 4346  omass 4347  oewordri 4355  oeworde 4356  oeordsuc 4357  oelim2 4358  oeoa 4360  oeoelem 4361  oeoe 4362  nnacl 4369  nnmcl 4370  nnecl 4371  nnacom 4373  nnmsucr 4380  nnmcom 4381  brecop 4447  eceqopreq 4454  th3qlem1 4455  f1oen2g 4535  f1domg 4537  fundmen 4569  unen 4575  mapxpen 4642  xpmapenlem4 4646  php 4660  pssnn 4681  domfi 4684  supsnALT 4735  inf3lem1 4758  inf3lem3 4760  noinfep 4786  r1tr 4800  rankr1 4820  aceq6a 4887  kmlem9 4919  numthlem 4929  zorn2lem1 4934  alephon 5015  alephordlem2 5023  alephordi 5024  alephsucdom 5030  alephle 5034  alephfplem3 5048  cflim 5059  indpi 5188  addcmpblnq 5206  mulcmpblnq 5207  genpprecl 5258  genpnmax 5264  prlem934b 5292  addcmpblnr 5335  recexsrlem 5366  map2psrpr 5374  pre-axmulgt0 5444  cnegexlem1 5499  addcani 5505  ltne 5670  ltle 5674  xrltle 5713  mulcani 5842  nnmulcl 6086  nnsubi 6102  xrsupsslem 6244  xrinfmsslem 6245  xrub 6248  supxrunb1 6257  supxrunb2 6258  nn0sub 6329  zaddcl 6333  zltp1le 6349  nneoi 6368  uzindOLD 6379  elioc2 6516  elico2 6517  elicc2 6518  uz11 6559  elfzlem 6601  fzopth 6632  om2uzuzi 6660  seq1rn2 6686  seqzrn2 6751  1exp 6779  expadd 6791  expmul 6792  sqrge0i 6903  sqr2irr 6930  crulem 6937  nn0abscl 7082  recan 7108  faclbnd 7148  bccl2 7174  fsum1s2 7213  climcmplem 7340  isumcl 7413  efcltlem2 7510  abspef01tlubi 7603  ruclem13 7734  infxpidmlem11 7774  tgss2 7849  cncnplem4 7987  blf 8054  lmsslem 8163  xplm 8186  xpcn 8187  cmsss 8208  grplactf1o 8339  nmosetre 8681  nmobndseqi 8695  orthcom 9250  hhcms 9348  hhsscms 9426  projlem13 9474  pjthlem11 9505  shsva 9560  hsupss 9585  shmodsi 9638  h1datomi 9780  pjrni 9925  nmopsetretALT 10070  nmfnsetre 10084  lnopcnbd 10244  pjclem4 10408  pj3si 10416  ssmd1 10519  atom1d 10561  chjatom 10565  atcvat4i 10606  cdj3lem2a 10645  cdj3lem3a 10648  findreccl 10702  nndivlub 10707  inpws1 10739  dupos1 10876  isexid2 10901  ismnd1 10927  uznzr 10967  mapudiscn 11015  subtopsin2 11067  efilcp2 11087  iint 11157  finsschain 11425  ordtypelem1 11427  ordtype 11434  hartog 11436  infenomsub 11450  cncomp 11494  locfindsc 11576  ist1-3 11604  fbssfg 11635  filssufillem 11655  filufint 11659  isfclus 11718  fipreima 11848  fzfi 11864  fsum00 11883  heiborlem11 12021  reheibor 12081

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 145

Copyright terms: Public domain