Theorem sylnbir 321

Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses

Ref	Expression
sylnbir.1	|- ( ps <-> ph )
sylnbir.2	|- ( -. ps -> ch )

Assertion

Ref	Expression
sylnbir	|- ( -. ph -> ch )

Proof of Theorem sylnbir

Step	Hyp	Ref	Expression
1		sylnbir.1	. . 3 |- ( ps <-> ph )
2	1	bicomi 214	. 2 |- ( ph <-> ps )
3		sylnbir.2	. 2 |- ( -. ps -> ch )
4	2, 3	sylnbi 320	1 |- ( -. ph -> ch )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  naecoms  2313  fvmptex  6294  f0cli  6370  1st2val  7194  2nd2val  7195  mpt2xopxprcov0  7343  rankvaln  8662  alephcard  8893  alephnbtwn  8894  cfub  9071  cardcf  9074  cflecard  9075  cfle  9076  cflim2  9085  cfidm  9097  itunitc1  9242  ituniiun  9244  domtriom  9265  alephreg  9404  pwcfsdom  9405  cfpwsdom  9406  adderpq  9778  mulerpq  9779  sumz  14453  sumss  14455  prod1  14674  prodss  14677  eleenn  25776  afvres  41252  afvco2  41256  ndmaovcl  41283