Theorem pm3.14 702

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 832. The converse holds for decidable propositions, as seen at pm3.13dc 900. (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 107	. . 3 |- ( ( ph /\ ps ) -> ph )
2	1	con3i 594	. 2 |- ( -. ph -> -. ( ph /\ ps ) )
3		simpr 108	. . 3 |- ( ( ph /\ ps ) -> ps )
4	3	con3i 594	. 2 |- ( -. ps -> -. ( ph /\ ps ) )
5	2, 4	jaoi 668	1 |- ( ( -. ph \/ -. ps ) -> -. ( ph /\ ps ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 102   \/ wo 661

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm3.1  703  xoranor  1308  difindiss  3218