Theorem imnan 697

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 642	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 124	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3	2	con2i 632	. 2 |- ( ( ph -> -. ps ) -> -. ( ph /\ ps ) )
4		pm3.2 139	. . 3 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
5	4	con3rr3 638	. 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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imnani  698  nan  699  mpnanrd  700  pm3.24  701  imanst  896  ianordc  907  pm5.17dc  912  dn1dc  969  xorbin  1429  xordc1  1438  alinexa  1652  dfrex2dc  2533  ralinexa  2569  rabeq0  3538  disj  3557  minel  3570  disjsn  3751  sotricim  4444  poirr2  5155  funun  5397  imadiflem  5435  imadif  5436  brprcneu  5663  2omotaplemap  7571  prltlu  7802  caucvgprlemnbj  7982  caucvgprprlemnbj  8008  suplocexprlemmu  8033  xrltnsym2  10127  fzp1nel  10438  fsumsplit  12093  sumsplitdc  12118  phiprmpw  12919  odzdvds  12943  pcdvdsb  13018  lgsne0  15911  lgsquadlem3  15952  bj-nnor  16506