Theorem pm3.14 670

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 799. The converse holds for decidable propositions, as seen at pm3.13dc 866. (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 102	. . 3 |- ( ( ph /\ ps ) -> ph )
2	1	con3i 562	. 2 |- ( -. ph -> -. ( ph /\ ps ) )
3		simpr 103	. . 3 |- ( ( ph /\ ps ) -> ps )
4	3	con3i 562	. 2 |- ( -. ps -> -. ( ph /\ ps ) )
5	2, 4	jaoi 636	1 |- ( ( -. ph \/ -. ps ) -> -. ( ph /\ ps ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 97   \/ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm3.1  671  xoranor  1268  difindiss  3191