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  2535  ralinexa  2571  rabeq0  3542  disj  3561  minel  3574  disjsn  3756  sotricim  4449  poirr2  5160  funun  5402  imadiflem  5440  imadif  5441  brprcneu  5668  2omotaplemap  7587  prltlu  7818  caucvgprlemnbj  7998  caucvgprprlemnbj  8024  suplocexprlemmu  8049  xrltnsym2  10146  fzp1nel  10460  fsumsplit  12118  sumsplitdc  12143  phiprmpw  12944  odzdvds  12968  pcdvdsb  13043  lgsne0  16037  lgsquadlem3  16078  bj-nnor  16632