Theorem imnan 694

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 640	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 124	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3	2	con2i 630	. 2 |- ( ( ph -> -. ps ) -> -. ( ph /\ ps ) )
4		pm3.2 139	. . 3 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
5	4	con3rr3 636	. 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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imnani  695  nan  696  mpnanrd  697  pm3.24  698  imanst  893  ianordc  904  pm5.17dc  909  dn1dc  966  xorbin  1426  xordc1  1435  alinexa  1649  dfrex2dc  2521  ralinexa  2557  rabeq0  3521  disj  3540  minel  3553  disjsn  3728  sotricim  4414  poirr2  5121  funun  5362  imadiflem  5400  imadif  5401  brprcneu  5620  2omotaplemap  7443  prltlu  7674  caucvgprlemnbj  7854  caucvgprprlemnbj  7880  suplocexprlemmu  7905  xrltnsym2  9990  fzp1nel  10300  fsumsplit  11918  sumsplitdc  11943  phiprmpw  12744  odzdvds  12768  pcdvdsb  12843  lgsne0  15717  lgsquadlem3  15758  bj-nnor  16098