Theorem 2falsed 714

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  715  bianfd  961  abvor0dc  3545  nn0eln0  4762  nntri3  6760  fin0  7179  2omap  7308  omp1eomlem  7424  ctssdccl  7441  ismkvnex  7485  xrlttri3  10178  nltpnft  10195  ngtmnft  10198  xrrebnd  10200  xltadd1  10257  xposdif  10263  xleaddadd  10268  xqltnle  10680  hashnncl  11212  zfz1isolemiso  11269  mod2eq1n2dvds  12624  m1exp1  12646  bitsmod  12701  pceq0  13079