Theorem 2falsed 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  710  bianfd  956  abvor0dc  3518  nn0eln0  4718  nntri3  6664  fin0  7073  omp1eomlem  7292  ctssdccl  7309  ismkvnex  7353  xrlttri3  10031  nltpnft  10048  ngtmnft  10051  xrrebnd  10053  xltadd1  10110  xposdif  10116  xleaddadd  10121  xqltnle  10526  hashnncl  11056  zfz1isolemiso  11102  mod2eq1n2dvds  12439  m1exp1  12461  bitsmod  12516  pceq0  12894  2omap  16594