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  2433  fvmptex  7029  f0cli  7117  1st2val  8043  2nd2val  8044  mpoxopxprcov0  8243  rankvaln  9840  alephcard  10111  alephnbtwn  10112  cfub  10290  cardcf  10293  cflecard  10294  cfle  10295  cflim2  10304  cfidm  10316  itunitc1  10461  ituniiun  10463  domtriom  10484  alephreg  10623  pwcfsdom  10624  cfpwsdom  10625  adderpq  10997  mulerpq  10998  sumz  15759  sumss  15761  prod1  15981  prodss  15984  newval  27895  leftval  27903  rightval  27904  lltropt  27912  madess  27916  oldssmade  27917  lrold  27936  fpwfvss  43430  grur1cld  44256  afvres  47189  afvco2  47193  ndmaovcl  47220
  Copyright terms: Public domain W3C validator