Theorem imnan 660

Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.)

Assertion

Ref	Expression
imnan	|- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )

Proof of Theorem imnan

Step	Hyp	Ref	Expression
1		pm3.2im 602	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 123	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3	2	con2i 593	. 2 |- ( ( ph -> -. ps ) -> -. ( ph /\ ps ) )
4		pm3.2 138	. . 3 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
5	4	con3rr3 599	. 2 |- ( -. ( ph /\ ps ) -> ( ph -> -. ps ) )
6	3, 5	impbii 125	1 |- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imnani  661  nan  662  pm3.24  663  imanst  780  imandc  825  ianordc  838  pm5.17dc  849  dn1dc  907  xorbin  1321  xordc1  1330  alinexa  1540  dfrex2dc  2372  ralinexa  2406  rabeq0  3318  disj  3337  minel  3350  disjsn  3510  sotricim  4161  poirr2  4839  funun  5073  imadiflem  5108  imadif  5109  brprcneu  5313  prltlu  7109  caucvgprlemnbj  7289  caucvgprprlemnbj  7315  xrltnsym2  9327  fzp1nel  9581  fsumsplit  10864  sumsplitdc  10889  phiprmpw  11539