Theorem pm3.14 765

Description: Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 911. The converse holds for decidable propositions, as seen at pm3.13dc 972. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)

Assertion

Ref	Expression
pm3.14	|- ( ( -. ph \/ -. ps ) -> -. ( ph /\ ps ) )

Proof of Theorem pm3.14

Step	Hyp	Ref	Expression
1		simpl 109	. . 3 |- ( ( ph /\ ps ) -> ph )
2	1	con3i 641	. 2 |- ( -. ph -> -. ( ph /\ ps ) )
3		simpr 110	. . 3 |- ( ( ph /\ ps ) -> ps )
4	3	con3i 641	. 2 |- ( -. ps -> -. ( ph /\ ps ) )
5	2, 4	jaoi 728	1 |- ( ( -. ph \/ -. ps ) -> -. ( ph /\ ps ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm3.1  766  xoranor  1426  difindiss  3485  swrdnd  11431