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

Theorem sylnbir 331
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 224 . 2 (𝜑𝜓)
3 sylnbir.2 . 2 𝜓𝜒)
42, 3sylnbi 330 1 𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206
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 207
This theorem is referenced by:  naecoms  2434  fvmptex  7030  f0cli  7118  1st2val  8042  2nd2val  8043  mpoxopxprcov0  8242  rankvaln  9839  alephcard  10110  alephnbtwn  10111  cfub  10289  cardcf  10292  cflecard  10293  cfle  10294  cflim2  10303  cfidm  10315  itunitc1  10460  ituniiun  10462  domtriom  10483  alephreg  10622  pwcfsdom  10623  cfpwsdom  10624  adderpq  10996  mulerpq  10997  sumz  15758  sumss  15760  prod1  15980  prodss  15983  newval  27894  leftval  27902  rightval  27903  lltropt  27911  madess  27915  oldssmade  27916  lrold  27935  fpwfvss  43425  grur1cld  44251  afvres  47184  afvco2  47188  ndmaovcl  47215
  Copyright terms: Public domain W3C validator