Theorem 2falsed 704

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 620	. 2 |- ( ph -> ( ps -> ch ) )
3		2falsed.2	. . 3 |- ( ph -> -. ch )
4	3	pm2.21d 620	. 2 |- ( ph -> ( ch -> ps ) )
5	2, 4	impbid 129	1 |- ( ph -> ( ps <-> ch ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  705  bianfd  951  abvor0dc  3492  nn0eln0  4686  nntri3  6606  fin0  7008  omp1eomlem  7222  ctssdccl  7239  ismkvnex  7283  xrlttri3  9954  nltpnft  9971  ngtmnft  9974  xrrebnd  9976  xltadd1  10033  xposdif  10039  xleaddadd  10044  xqltnle  10447  hashnncl  10977  zfz1isolemiso  11021  mod2eq1n2dvds  12305  m1exp1  12327  bitsmod  12382  pceq0  12760  2omap  16132