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  3484  nn0eln0  4668  nntri3  6583  fin0  6982  omp1eomlem  7196  ctssdccl  7213  ismkvnex  7257  xrlttri3  9919  nltpnft  9936  ngtmnft  9939  xrrebnd  9941  xltadd1  9998  xposdif  10004  xleaddadd  10009  xqltnle  10410  hashnncl  10940  zfz1isolemiso  10984  mod2eq1n2dvds  12190  m1exp1  12212  bitsmod  12267  pceq0  12645  2omap  15932