Theorem syl6bi 231

Description: A mixed syllogism inference.

Hypotheses

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

Assertion

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

Proof of Theorem syl6bi

Step	Hyp	Ref	Expression
1		syl6bi.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimpd 170	. 2 |- (ph -> (ps -> ch))
3		syl6bi.2	. 2 |- (ch -> th)
4	2, 3	syl6 25	1 |- (ph -> (ps -> th))

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

This theorem is referenced by:  ax11i 1498  a12lem1 1767  2eu2 1854  reu6 2443  ra4sbc 2536  sseq0 2903  disjpss 2924  rzalOLD 2971  preq12b 3154  prel12 3155  elinti 3223  zfrepclf 3434  dtru 3498  opprc3 3543  opth2 3546  frirr 3634  ordsseleqOLD 3688  ordtr2 3708  nsuceq0 3749  ordssun 3769  ordequn 3770  reuuni4 3813  ordssonOLD 3868  limuni3 3936  peano5 3975  opeldm 4160  elreldm 4185  funopg 4454  funimass2 4492  fvco 4736  funfvop 4776  fconstfv 4825  elunirnALT 4845  oaordi 5227  oa00 5241  oalimcl 5242  nnaordex 5306  nnawordex 5307  oaabs 5309  erth 5340  ecopoprtrn 5370  riotabidva 5575  opthreg 5709  inf3lemd 5718  inf3lem2 5720  inf3lem6 5724  r1tr 5765  rankr1 5785  r1pwcl 5798  karden 5856  omsubdom 5882  infenomsub 5889  aceq5lem4 5900  kmlem2 5928  kmlem12 5938  brdom6disj 5967  carden 5981  cfeq0 6062  addnidpi 6180  indpi 6186  ordpipq 6208  ltsopq 6227  addcanpr 6304  prlem936 6307  suplem1pr 6313  suplem2pr 6314  ltsrpr 6338  ltsosr 6355  sqgt0sr 6367  addcani 6505  addcaniOLD 6506  leltne 6691  ltlen 6692  ltnsym 6702  xrleltne 6733  mulcani 6878  lt2msqi 7064  lt1nnn 7130  infm3 7263  nnunb 7279  btwnz 7428  zq 7440  modadd1 7518  modmul1 7519  modirr 7522  iccleub 7551  elioore 7554  uz11 7601  elfzlem 7643  elfzel2g 7650  elfz3nn0 7669  fznn0sub 7670  creur 7992  creui 7993  seq1bndi 8162  bccl2 8223  caucvglem2 8418  caucvglem5 8421  caucvglem6 8422  geoisumr 8505  alephexp1 8853  tg2 8891  unitg 8893  tgcl 8894  iincld 8955  neii1 8997  neii2 8998  cnsscnp 9049  opni 9141  metcnpi 9168  metcnpi2 9169  metcni 9172  caun0 9223  lmfss 9226  lmcl 9227  iscms2lem4 9270  gapmlem 9461  nvex 9562  nmlno0lem 9793  sineq0re 10067  efifolem6 10081  twpar2 10149  dif1enOLD 10173  fiv 10212  fiiu2 10220  oefil2 10275  fgbas 10286  fbfgss 10288  neifil 10302  hausfillim2 10325  usinuniop 10341  clmgm 10368  smgrpmgm 10382  smgrpass 10383  ismnd2 10392  on1el3 10412  dvrunz 10419  normgt0OLD 10626  normgt0 10627  ocin 10802  nmlnop0iALT 11557  nmopun 11576  lnopconi 11600  lnfnconi 11627  cvpss 11857  cvnbtwn 11858  atcvati 11958  mdsymlem6 11980  bnj112 12457  bnj1343 13067  fz1eqblem 13608  0dvds 13675  gcdneg 13732  algcvga 13747  dford4lem2 13860  frxp 13951  sltsgn1 14002  sltsgn2 14003  sltintdifex 14004  axfelem12 14042  altopth2sn 14091  uninqs 14340  infi1 14343  fiiu 14344  ref4w 14370  isunscov 14386  prj1 14395  resrelfld 14448  reltrncnv 14457  repfuntw 14502  repcpwti 14503  unprj 14511  prl2 14514  nZdef 14527  jop 14532  mop 14533  labs1 14536  labs2 14538  preodom2 14567  preoran2 14571  altprs2 14577  int2pre 14578  prltub 14602  supdef 14604  suplub2 14616  geme2 14617  dutos1 14626  dfps2 14634  pospos 14635  iscomb 14690  mndid 14718  mndio 14719  mndass 14720  mgmrddd 14727  gaplc 14731  curgrpact 14735  fprodneg 14741  fprodsub 14742  svs2 14829  clsrebb 14844  elioo1t3 14846  truni3 14851  unint2t 14866  cnvhmphb 14880  hmeogrp 14892  top2ind 14897  top2usne 14898  stoig2b 14906  subtopsin2 14907  filint2 14923  cnfilca 14927  rcfpfillem3 14930  fbaslim2 14936  limvinlv 14941  conttnf 14944  bwt2 14960  clindistop 14962  topsinind 14967  iintlem1 15010  lteqtpos 15024  mamb 15030  dualcat2lem 15129  dualded2lem 15130  dualalg 15131  obsubc2 15198  idsubc 15199  domsubc 15200  codsubc 15201  subctct 15202  morsubc 15203  cmpsubc 15204  tarax1 15216  tarax2 15217  tarax3 15218  tarax3c 15224  tarsuc2 15245  tartarmap 15265  subtsm 15267  cardtar 15281  elcarelcl 15283  fnctartar 15284  fnctartar2 15285  ioodisj 15364  omsubdomOLD 15391  infenomsubOLD 15398  cldbnd 15410  alexsublem2 15438  alexsub 15441  fclusbas 15610  raleqfn 15672  cover2 15673  findcard2 15745  fimax 15746  inficl 15757  sdclem2 15810  sdc 15811  fdc 15812  heiborlem11 15965  heiborlem31 15985  ismrer1 16024  phtpcdm 16061  pcohtpy 16083  0ring 16175  erex 16262  prtlem16 16272  iotavalsb 16398  smoge 16454  joinlem 16817  meetlem 16824  cmtbr3 16975  atomnle 17016  cvratlem 17061  linepsub 17232  elpaddati 17266

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 164

Copyright terms: Public domain