Theorem 2falsed 702

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  703  bianfd  948  abvor0dc  3448  nn0eln0  4621  nntri3  6501  fin0  6888  omp1eomlem  7096  ctssdccl  7113  ismkvnex  7156  xrlttri3  9800  nltpnft  9817  ngtmnft  9820  xrrebnd  9822  xltadd1  9879  xposdif  9885  xleaddadd  9890  hashnncl  10778  zfz1isolemiso  10822  mod2eq1n2dvds  11887  m1exp1  11909  pceq0  12324