Theorem syl5bir 226

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

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

This theorem is referenced by:  syl5cbir 227  orbi1r 1124  hbsb4tOLD 1460  pm2.61ne 1922  pm2.61neOLD 1923  unineq 2671  ssopab2 3388  sotrieqOLD 3432  ordtri3 3512  ordtri3OLD 3513  limelon 3542  eufromeq3 3641  alxfr 3647  eldifpw 3665  ssonuni 3683  onsucuni2 3725  ordzsl 3738  tfindsg 3755  limom 3778  findsg 3791  vtoclrbr 3844  vtoclrbrOLD 3845  ralxp 3852  fcoOLD 4385  ndmfv 4513  fvco 4547  isomin 4687  isofrlem 4689  tfrlem1 4930  tfrlem11 4940  oacl 5026  omcl 5027  omclOLD 5028  oecl 5029  oeclOLD 5030  oa0r 5031  om0r 5032  om1r 5035  oe1m 5037  oaordi 5038  oawordri 5043  oaass 5054  omwordri 5062  odi 5069  omass 5070  oewordri 5078  oeworde 5079  oeordsuc 5080  oelim2 5081  oeoa 5083  oeoelem 5084  oeoe 5085  nnacl 5092  nnaclOLD 5093  nnmclOLD 5095  nneclOLD 5097  nnacom 5099  nnmsucr 5106  nnmsucrOLD 5107  nnmcom 5108  nnmcomOLD 5109  brecop 5176  eceqopreq 5183  th3qlem1 5184  f1oen2g 5264  f1domg 5266  fundmen 5298  unen 5304  mapxpen 5399  xpmapenlem4 5403  php 5417  pssnn 5438  domfi 5441  supsnALT 5492  ordtypelem1 5494  ordtype 5501  hartog 5503  inf3lem1 5528  inf3lem3 5530  noinfep 5556  r1tr 5574  rankr1 5594  alephon 5672  infenomsub 5685  aceq6a 5699  kmlem9 5731  numthlem 5741  zorn2lem1 5746  alephordlem2 5817  alephordi 5818  alephsucdom 5824  alephle 5828  alephfplem3 5842  cflim 5853  indpi 5982  addcmpblnq 6000  mulcmpblnq 6001  genpprecl 6052  genpnmax 6058  prlem934b 6086  addcmpblnr 6129  recexsrlem 6160  map2psrpr 6168  pre-axmulgt0 6239  cnegexlem1 6295  addcaniOLD 6302  ltne 6482  ltle 6486  xrltle 6530  mulcani 6674  nnmulcl 6919  nnsubi 6935  xrsupsslem 7080  xrinfmsslem 7081  xrub 7084  supxrunb1 7093  supxrunb2 7094  nn0sub 7165  zaddcl 7169  zltp1le 7185  nneoi 7204  uzindOLD 7215  elioc2 7353  elico2 7354  elicc2 7355  uz11 7396  elfzlem 7438  fzopth 7469  om2uzuzi 7503  seq1rn2 7529  seqzrn2 7594  1exp 7622  expadd 7634  expmul 7635  sqrge0i 7747  sqr2irr 7774  crulem 7781  nn0abscl 7926  recan 7952  faclbnd 7992  bccl2 8018  fsum1s2 8065  climcmplem 8192  isumcl 8265  efcltlem2 8362  abspef01tlubi 8455  ruclem13 8586  infxpidmlem11 8626  tgss2 8702  cncnplem4 8849  blf 8916  lmsslem 9025  xplm 9048  xpcn 9049  cmsss 9070  grplactf1o 9201  nmosetre 9561  nmobndseqi 9575  fbssfg 10077  cncomp 10123  isexid2 10164  ismnd1 10183  uznzr 10208  orthcom 10399  hhcms 10497  hhsscms 10575  projlem13 10623  pjthlem11 10654  shsva 10709  hsupss 10734  shmodsi 10787  h1datomi 10929  pjrni 11074  nmopsetretALT 11219  nmfnsetre 11233  lnopcnbd 11394  pjclem4 11564  pj3si 11572  ssmd1 11675  atom1d 11717  chjatom 11721  atcvat4i 11761  cdj3lem2a 11800  cdj3lem3a 11803  bnj1115 12718  bnj594 13092  bnj936 13128  bnj1128 13220  dvdstr 13479  alzdvds 13487  elsnres 13619  dfon2lem6 13645  predpoirr 13700  predfrirr 13701  trcllem1 13725  trcltr 13728  poxp 13741  soxp 13742  frxp 13743  wfrlem14 13762  axdenselem8 13816  findreccl 13984  nndivlub 13989  inpws1 14073  unpam2 14154  onsubcum 14172  cmprelid2 14177  fvsnn 14179  cnveq2 14184  cnveq3 14185  fopab2g 14212  repfuntw 14228  repcpwti 14229  cbicplem 14234  unprj 14237  prl2 14240  dupre2 14308  dupos1 14309  ubos2 14320  mxlelt2 14328  mnlelt2 14330  mxlmnl2 14334  defgelem 14335  defselem 14336  defge 14337  defse 14338  dutos2 14351  istoset2 14353  defge2 14362  dfdir2 14365  dffprod 14394  fprod1s2 14402  ablcomgrp 14425  grpdrcan 14461  mapudiscn 14593  subtopsin2 14626  ptincpw 14631  efilcp2 14640  cnpfillim4 14661  trhom 14697  tpgprop2 14701  cntrsetlem 14709  iint 14722  lvsovso 14734  dualded 14814  cptarc 14924  valdom 14943  fnctartar 14966  fnctartar2 14967  isseg2 14987  finsschain 15055  ordtypelem1OLD 15057  ordtypeOLD 15064  hartogOLD 15066  infenomsubOLD 15080  locfindsc 15197  ist1-3 15225  filssufillem 15252  filufint 15256  isfclus 15288  eqfnun 15387  ixpssmapg 15408  fipreima 15438  fzfi 15468  seq1eq2 15499  fsum00 15502  txmet 15607  heiborlem11 15647  reheibor 15707  exidreslem 15712  risci 15823  prtlem11 15950  prtlem16 15954  prtlem15 15963  cvrat4 16806

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 163

Copyright terms: Public domain