Theorem 2falsed 691

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 608	. 2 |- ( ph -> ( ps -> ch ) )
3		2falsed.2	. . 3 |- ( ph -> -. ch )
4	3	pm2.21d 608	. 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 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.21ni  692  bianfd  932  abvor0dc  3386  nn0eln0  4533  nntri3  6393  fin0  6779  omp1eomlem  6979  ctssdccl  6996  ismkvnex  7029  xrlttri3  9583  nltpnft  9597  ngtmnft  9600  xrrebnd  9602  xltadd1  9659  xposdif  9665  xleaddadd  9670  hashnncl  10542  zfz1isolemiso  10582  mod2eq1n2dvds  11576  m1exp1  11598