Theorem syl6bi 212

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 151	. 2 |- (ph -> (ps -> ch))
3		syl6bi.2	. 2 |- (ch -> th)
4	2, 3	syl6 22	1 |- (ph -> (ps -> th))

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

This theorem is referenced by:  ax11i 1175  a12lem1 1415  2eu2 1490  reu3 1977  ra4sbc 2047  disjpss 2372  rzal 2409  preq12b 2548  prel12 2549  zfrepclf 2773  dtru 2831  opprc3 2873  opth2 2876  frirr 2954  ordsseleq 3004  nsuceq0 3053  ordssun 3069  ordequn 3070  reuuni4 3110  ordsson 3145  limuni3 3206  peano5 3241  opeldm 3405  elreldm 3425  funopg 3652  funimass2 3678  fvco 3885  funfvop 3917  fconstfv 3963  elunirnALT 3983  oaordi 4316  oa00 4329  oalimcl 4330  nnaordex 4389  nnawordex 4390  oaabs 4392  erth 4422  ecopoprtrn 4452  opthreg 4749  inf3lemd 4757  inf3lem2 4759  inf3lem6 4763  r1tr 4800  rankr1 4820  r1pwcl 4833  karden 4872  aceq5lem4 4884  kmlem2 4912  kmlem12 4922  brdom6disj 4951  carden 4979  cfeq0 5064  addnidpi 5182  indpi 5188  ordpipq 5210  ltsopq 5229  addcanpr 5306  prlem936 5309  suplem1pr 5315  suplem2pr 5316  ltsrpr 5340  ltsosr 5357  sqgt0sr 5369  addcani 5505  leltne 5675  ltlen 5676  ltnsym 5686  xrleltne 5712  mulcani 5842  lt2msqi 6026  lt1nnn 6092  infm3 6222  nnunb 6238  btwnz 6387  zq 6399  modadd1 6477  modmul1 6478  modirr 6481  elioore 6512  uz11 6559  elfzlem 6601  elfzel2g 6608  elfz3nn0 6627  fznn0sub 6628  creur 6943  creui 6944  seq1bndi 7113  bccl2 7174  caucvglem2 7361  caucvglem5 7364  caucvglem6 7365  geoisumr 7448  alephexp1 7796  tg2 7833  unitg 7835  tgcl 7836  iincld 7889  neii1 7931  neii2 7932  cnsscnp 7982  opni 8074  metcnpi 8101  metcnpi2 8102  metcni 8105  caun0 8156  lmfss 8159  lmcl 8160  iscms2lem4 8203  nvex 8477  nmlno0lem 8708  sineq0re 8985  efifolem6 8999  normgt0OLD 9269  normgt0 9270  ocin 9445  nmlnop0iALT 10199  nmopun 10218  lnopconi 10242  lnfnconi 10269  cvpss 10493  cvnbtwn 10494  atcvati 10595  mdsymlem6 10617  uninqs 10730  infi1 10735  fiiu 10738  ref3w 10772  twpar2 10773  scprefat 10783  isunscov 10796  prj1 10809  jop 10832  mop 10833  labs1 10836  labs2 10838  fiv 10849  fiiu2 10852  lteqtpos 10880  pospos 10882  smgrpmgm 10912  smgrpass 10913  ismnd2 10928  mndid 10929  mndio 10930  mndass 10931  on1el3 10962  dvrunz 10970  clsrebb 10993  elioo1t3 10996  truni3 11001  cnvhmphb 11032  hmeogrp 11044  top2ind 11050  top2usne 11051  subtopsin2 11067  oefil2 11079  neifil 11080  filint2 11084  cnfilca 11088  rcfpfillem3 11091  bwt2 11123  usinuniop 11128  clindistop 11131  topsinind 11136  iintlem1 11155  obsubc2 11304  idsubc 11305  domsubc 11306  codsubc 11307  subctct 11308  morsubc 11309  cmpsubc 11310  iccleub 11411  ioodisj 11413  omsubdom 11443  infenomsub 11450  cldbnd 11462  alexsublem2 11497  alexsub 11500  fgbas 11636  fbfgss 11640  fclusbas 11722  gapmlem 11783  raleqfn 11790  dif1en 11833  inficl 11849  sdclem2 11876  sdc 11877  heiborlem11 12021  heiborlem31 12041  ismrer1 12080  phtpcdm 12103

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