Theorem 2falsed 710

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  711  bianfd  957  abvor0dc  3532  nn0eln0  4742  nntri3  6730  fin0  7142  2omap  7269  omp1eomlem  7385  ctssdccl  7402  ismkvnex  7446  xrlttri3  10130  nltpnft  10147  ngtmnft  10150  xrrebnd  10152  xltadd1  10209  xposdif  10215  xleaddadd  10220  xqltnle  10627  hashnncl  11158  zfz1isolemiso  11211  mod2eq1n2dvds  12565  m1exp1  12587  bitsmod  12642  pceq0  13020