HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 syl6bi.1 . . 3 |- (ph -> (ps <-> ch))
21biimpd 153 . 2 |- (ph -> (ps -> ch))
3 syl6bi.2 . 2 |- (ch -> th)
42, 3syl6 22 1 |- (ph -> (ps -> th))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146
This theorem is referenced by:  ax11i 1134  a12lem1 1369  2eu2 1443  reu3 1921  ra4sbc 1987  disjpss 2309  rzal 2345  preq12b 2474  prel12 2475  zfrepclf 2689  dtruALT 2738  opprc3 2787  opth2 2789  reuuni4 2877  frirr 2914  ordsseleq 2966  ordsson 2981  nsuceq0 3043  ordssun 3069  ordequn 3070  limuni3 3113  peano5 3143  opeldm 3303  elreldm 3327  funopg 3533  funimass2 3559  fvco 3759  funfvop 3788  fconstfv 3834  elunirnALT 3854  oaordi 4164  oa00 4177  oalimcl 4178  nnaordex 4233  nnawordex 4234  oaabs 4236  erth 4266  ecopoprtrn 4295  opthreg 4576  inf3lemd 4584  inf3lem2 4586  inf3lem6 4590  r1tr 4626  rankr1 4646  r1pwcl 4659  karden 4698  aceq5lem4 4710  kmlem2 4738  kmlem12 4748  brdom6disj 4777  carden 4803  cfeq0 4886  addnidpi 5000  indpi 5006  ordpipq 5028  ltsopq 5047  addcanpr 5124  prlem936 5127  suplem1pr 5133  suplem2pr 5134  ltsrpr 5158  ltsosr 5175  sqgt0sr 5187  addcan 5323  leltnet 5494  ltlent 5495  ltnsymt 5505  xrleltnet 5531  mulcan 5659  lt2msq 5829  lt1nnn 5895  infm3 6001  nnunb 6017  btwnz 6163  zqt 6198  uz11t 6364  elfzlem 6405  elfzel2g 6412  elfz3nn0t 6429  fznn0subt 6430  creur 6673  creui 6674  seq1bnd 6847  bccl2t 6909  caucvglem2 7094  caucvglem5 7097  caucvglem6 7098  geoisumr 7178  alephexp1 7526  tg2t 7563  unitgt 7565  tgclt 7566  iincld 7621  neii1 7662  neii2 7663  cnsscnp 7711  opni 7804  metcnpi 7829  metcnpi2 7830  metcni 7833  caun0 7880  lmfss 7883  lmcl 7884  iscms2lem4 7926  nvex 8169  nmlno0lem 8385  efifolem6 8642  normgt0tOLD 8914  normgt0t 8915  ocin 9085  nmlnop0ALT 9835  nmopunt 9854  lnopcon 9878  lnfncon 9905  cvpsst 10122  cvnbtwnt 10123  atcvat 10221  mdsymlem6 10243  uninqs 10342  infi1 10347  fiiu 10350  fiv 10374  fiiu2 10377  clsrebb 10380  elioo1t3 10383  cnvhmphb 10413  hmeogrp 10425  oefil2 10441  neifil 10442  filint2 10446  cnfilca 10451  iintlem1 10476
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