Theorem imnan 680

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 627	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 123	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3	2	con2i 617	. 2 |- ( ( ph -> -. ps ) -> -. ( ph /\ ps ) )
4		pm3.2 138	. . 3 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
5	4	con3rr3 623	. 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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imnani  681  nan  682  pm3.24  683  imanst  874  ianordc  885  pm5.17dc  890  dn1dc  945  xorbin  1363  xordc1  1372  alinexa  1583  dfrex2dc  2429  ralinexa  2465  rabeq0  3397  disj  3416  minel  3429  disjsn  3593  sotricim  4253  poirr2  4939  funun  5175  imadiflem  5210  imadif  5211  brprcneu  5422  prltlu  7319  caucvgprlemnbj  7499  caucvgprprlemnbj  7525  suplocexprlemmu  7550  xrltnsym2  9610  fzp1nel  9915  fsumsplit  11208  sumsplitdc  11233  phiprmpw  11934  bj-nnor  13117