Theorem 2falsed 692

Description: Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.)

Hypotheses

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

Assertion

Ref	Expression
2falsed	|- ( ph -> ( ps <-> ch ) )

Proof of Theorem 2falsed

Step	Hyp	Ref	Expression
1		2falsed.1	. . 3 |- ( ph -> -. ps )
2	1	pm2.21d 609	. 2 |- ( ph -> ( ps -> ch ) )
3		2falsed.2	. . 3 |- ( ph -> -. ch )
4	3	pm2.21d 609	. 2 |- ( ph -> ( ch -> ps ) )
5	2, 4	impbid 128	1 |- ( ph -> ( ps <-> ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.21ni  693  bianfd  937  abvor0dc  3427  nn0eln0  4591  nntri3  6456  fin0  6842  omp1eomlem  7050  ctssdccl  7067  ismkvnex  7110  xrlttri3  9724  nltpnft  9741  ngtmnft  9744  xrrebnd  9746  xltadd1  9803  xposdif  9809  xleaddadd  9814  hashnncl  10698  zfz1isolemiso  10738  mod2eq1n2dvds  11801  m1exp1  11823  pceq0  12230