Theorem 2falsed 707

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  708  bianfd  954  abvor0dc  3515  nn0eln0  4712  nntri3  6651  fin0  7055  omp1eomlem  7272  ctssdccl  7289  ismkvnex  7333  xrlttri3  10005  nltpnft  10022  ngtmnft  10025  xrrebnd  10027  xltadd1  10084  xposdif  10090  xleaddadd  10095  xqltnle  10499  hashnncl  11029  zfz1isolemiso  11074  mod2eq1n2dvds  12405  m1exp1  12427  bitsmod  12482  pceq0  12860  2omap  16418