Theorem syl6bi 214

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

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

This theorem is referenced by:  ax11i 1140  a12lem1 1378  2eu2 1453  reu3 1934  ra4sbc 2000  disjpss 2323  rzal 2359  preq12b 2487  prel12 2488  zfrepclf 2704  dtruALT 2754  opprc3 2803  opth2 2806  reuuni4 2893  frirr 2930  ordsseleq 2982  ordsson 2997  nsuceq0 3059  ordssun 3085  ordequn 3086  limuni3 3129  peano5 3159  opeldm 3320  elreldm 3344  funopg 3553  funimass2 3579  fvco 3780  funfvop 3809  fconstfv 3855  elunirnALT 3875  oaordi 4186  oa00 4199  oalimcl 4200  nnaordex 4255  nnawordex 4256  oaabs 4258  erth 4288  ecopoprtrn 4317  opthreg 4613  inf3lemd 4621  inf3lem2 4623  inf3lem6 4627  r1tr 4664  rankr1 4684  r1pwcl 4697  karden 4736  aceq5lem4 4748  kmlem2 4776  kmlem12 4786  brdom6disj 4815  carden 4841  cfeq0 4926  addnidpi 5040  indpi 5046  ordpipq 5068  ltsopq 5087  addcanpr 5164  prlem936 5167  suplem1pr 5173  suplem2pr 5174  ltsrpr 5198  ltsosr 5215  sqgt0sr 5227  addcan 5363  leltnet 5533  ltlent 5534  ltnsymt 5544  xrleltnet 5570  mulcan 5698  mulcanOLD 5699  lt2msq 5883  lt1nnn 5949  infm3 6056  nnunb 6072  btwnz 6217  zqt 6261  eliooret 6387  uz11t 6433  elfzlem 6474  elfzel2g 6481  elfz3nn0t 6498  fznn0subt 6499  creur 6743  creui 6744  seq1bnd 6910  bccl2t 6971  caucvglem2 7158  caucvglem5 7161  caucvglem6 7162  geoisumr 7243  alephexp1 7586  tg2t 7620  unitgt 7622  tgclt 7623  iincld 7676  neii1 7718  neii2 7719  cnsscnp 7769  opni 7861  metcnpi 7887  metcnpi2 7888  metcni 7891  caun0 7942  lmfss 7945  lmcl 7946  iscms2lem4 7989  nvex 8226  nmlno0lem 8449  efifolem6 8722  normgt0tOLD 8988  normgt0t 8989  ocin 9164  nmlnop0ALT 9915  nmopunt 9934  lnopcon 9958  lnfncon 9985  cvpsst 10207  cvnbtwnt 10208  atcvat 10308  mdsymlem6 10330  uninqs 10436  infi1 10441  fiiu 10444  fiv 10470  fiiu2 10473  clsrebb 10479  elioo1t3 10482  cnvhmphb 10512  hmeogrp 10524  top2ind 10534  top2usne 10535  oefil2 10552  neifil 10553  filint2 10557  cnfilca 10562  rcfpfillem3 10565  iintlem1 10603

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