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 1138  a12lem1 1376  2eu2 1450  reu3 1931  ra4sbc 1997  disjpss 2319  rzal 2355  preq12b 2483  prel12 2484  zfrepclf 2699  dtruALT 2748  opprc3 2797  opth2 2800  reuuni4 2887  frirr 2924  ordsseleq 2976  ordsson 2991  nsuceq0 3053  ordssun 3079  ordequn 3080  limuni3 3123  peano5 3153  opeldm 3314  elreldm 3338  funopg 3547  funimass2 3573  fvco 3774  funfvop 3803  fconstfv 3849  elunirnALT 3869  oaordi 4180  oa00 4193  oalimcl 4194  nnaordex 4249  nnawordex 4250  oaabs 4252  erth 4282  ecopoprtrn 4311  opthreg 4604  inf3lemd 4612  inf3lem2 4614  inf3lem6 4618  r1tr 4654  rankr1 4674  r1pwcl 4687  karden 4726  aceq5lem4 4738  kmlem2 4766  kmlem12 4776  brdom6disj 4805  carden 4831  cfeq0 4914  addnidpi 5028  indpi 5034  ordpipq 5056  ltsopq 5075  addcanpr 5152  prlem936 5155  suplem1pr 5161  suplem2pr 5162  ltsrpr 5186  ltsosr 5203  sqgt0sr 5215  addcan 5351  leltnet 5521  ltlent 5522  ltnsymt 5532  xrleltnet 5558  mulcan 5686  mulcanOLD 5687  lt2msq 5881  lt1nnn 5947  infm3 6054  nnunb 6070  btwnz 6215  zqt 6260  eliooret 6386  uz11t 6432  elfzlem 6473  elfzel2g 6480  elfz3nn0t 6497  fznn0subt 6498  creur 6742  creui 6743  seq1bnd 6910  bccl2t 6971  caucvglem2 7158  caucvglem5 7161  caucvglem6 7162  geoisumr 7243  alephexp1 7584  tg2t 7621  unitgt 7623  tgclt 7624  iincld 7679  neii1 7721  neii2 7722  cnsscnp 7772  opni 7864  metcnpi 7890  metcnpi2 7891  metcni 7894  caun0 7945  lmfss 7948  lmcl 7949  iscms2lem4 7992  nvex 8230  nmlno0lem 8453  efifolem6 8727  normgt0tOLD 8993  normgt0t 8994  ocin 9169  nmlnop0ALT 9920  nmopunt 9939  lnopcon 9963  lnfncon 9990  cvpsst 10212  cvnbtwnt 10213  atcvat 10313  mdsymlem6 10335  uninqs 10441  infi1 10447  infi1OLD 10448  fiiu 10453  fiiuOLD 10454  fiv 10482  fivOLD 10483  fiiu2 10488  fiiu2OLD 10489  clsrebb 10493  elioo1t3 10496  cnvhmphb 10526  hmeogrp 10538  top2ind 10548  top2usne 10549  oefil2 10567  neifil 10568  filint2 10574  filint2OLD 10575  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem3 10589  rcfpfillem3OLD 10590  iintlem1 10632

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