MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylnbir Unicode version

Theorem sylnbir 307
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.)
Hypotheses
Ref Expression
sylnbir.1
sylnbir.2
Assertion
Ref Expression
sylnbir

Proof of Theorem sylnbir
StepHypRef Expression
1 sylnbir.1 . . 3
21bicomi 202 . 2
3 sylnbir.2 . 2
42, 3sylnbi 306 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  naecoms  2053  fvmptex  5966  f0cli  6042  1st2val  6826  2nd2val  6827  mpt2xopxprcov0  6964  rankvaln  8238  alephcard  8472  alephnbtwn  8473  cfub  8650  cardcf  8653  cflecard  8654  cfle  8655  cflim2  8664  cfidm  8676  itunitc1  8821  ituniiun  8823  domtriom  8844  alephreg  8978  pwcfsdom  8979  cfpwsdom  8980  adderpq  9355  mulerpq  9356  sumz  13544  sumss  13546  prod1  13751  prodss  13754  eleenn  24199  afvres  32257  afvco2  32261  ndmaovcl  32288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator