Theorem imnan 692

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  693  nan  694  pm3.24  695  imanst  890  ianordc  901  pm5.17dc  906  dn1dc  963  xorbin  1404  xordc1  1413  alinexa  1626  dfrex2dc  2497  ralinexa  2533  rabeq0  3490  disj  3509  minel  3522  disjsn  3695  sotricim  4371  poirr2  5076  funun  5316  imadiflem  5354  imadif  5355  brprcneu  5571  2omotaplemap  7371  prltlu  7602  caucvgprlemnbj  7782  caucvgprprlemnbj  7808  suplocexprlemmu  7833  xrltnsym2  9918  fzp1nel  10228  fsumsplit  11751  sumsplitdc  11776  phiprmpw  12577  odzdvds  12601  pcdvdsb  12676  lgsne0  15548  lgsquadlem3  15589  bj-nnor  15707