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  4711  nntri3  6641  fin0  7043  omp1eomlem  7257  ctssdccl  7274  ismkvnex  7318  xrlttri3  9989  nltpnft  10006  ngtmnft  10009  xrrebnd  10011  xltadd1  10068  xposdif  10074  xleaddadd  10079  xqltnle  10482  hashnncl  11012  zfz1isolemiso  11056  mod2eq1n2dvds  12385  m1exp1  12407  bitsmod  12462  pceq0  12840  2omap  16318