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  3516  nn0eln0  4716  nntri3  6660  fin0  7067  omp1eomlem  7284  ctssdccl  7301  ismkvnex  7345  xrlttri3  10022  nltpnft  10039  ngtmnft  10042  xrrebnd  10044  xltadd1  10101  xposdif  10107  xleaddadd  10112  xqltnle  10517  hashnncl  11047  zfz1isolemiso  11093  mod2eq1n2dvds  12430  m1exp1  12452  bitsmod  12507  pceq0  12885  2omap  16530