Theorem 2falsed 703

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  704  bianfd  950  abvor0dc  3483  nn0eln0  4667  nntri3  6582  fin0  6981  omp1eomlem  7195  ctssdccl  7212  ismkvnex  7256  xrlttri3  9918  nltpnft  9935  ngtmnft  9938  xrrebnd  9940  xltadd1  9997  xposdif  10003  xleaddadd  10008  xqltnle  10408  hashnncl  10938  zfz1isolemiso  10982  mod2eq1n2dvds  12161  m1exp1  12183  bitsmod  12238  pceq0  12616  2omap  15894