Theorem imnan 691

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 638	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 124	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3	2	con2i 628	. 2 |- ( ( ph -> -. ps ) -> -. ( ph /\ ps ) )
4		pm3.2 139	. . 3 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
5	4	con3rr3 634	. 2 |- ( -. ( ph /\ ps ) -> ( ph -> -. ps ) )
6	3, 5	impbii 126	1 |- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imnani  692  nan  693  pm3.24  694  imanst  889  ianordc  900  pm5.17dc  905  dn1dc  962  xorbin  1395  xordc1  1404  alinexa  1617  dfrex2dc  2488  ralinexa  2524  rabeq0  3481  disj  3500  minel  3513  disjsn  3685  sotricim  4359  poirr2  5063  funun  5303  imadiflem  5338  imadif  5339  brprcneu  5554  2omotaplemap  7340  prltlu  7571  caucvgprlemnbj  7751  caucvgprprlemnbj  7777  suplocexprlemmu  7802  xrltnsym2  9886  fzp1nel  10196  fsumsplit  11589  sumsplitdc  11614  phiprmpw  12415  odzdvds  12439  pcdvdsb  12514  lgsne0  15363  lgsquadlem3  15404  bj-nnor  15464