Theorem imnan 701

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 646	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 124	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3	2	con2i 636	. 2 |- ( ( ph -> -. ps ) -> -. ( ph /\ ps ) )
4		pm3.2 139	. . 3 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
5	4	con3rr3 642	. 2 |- ( -. ( ph /\ ps ) -> ( ph -> -. ps ) )
6	3, 5	impbii 126	1 |- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  imnani  702  nan  703  mpnanrd  704  pm3.24  705  imanst  900  ianordc  911  pm5.17dc  916  dn1dc  973  xorbin  1433  xordc1  1442  alinexa  1656  dfrex2dc  2541  ralinexa  2577  rabeq0  3552  disj  3573  minel  3586  disjsn  3771  sotricim  4470  poirr2  5183  funun  5425  imadiflem  5463  imadif  5464  brprcneu  5691  2omotaplemap  7629  prltlu  7860  caucvgprlemnbj  8040  caucvgprprlemnbj  8066  suplocexprlemmu  8091  xrltnsym2  10213  fzp1nel  10528  fsumsplit  12199  sumsplitdc  12224  phiprmpw  13029  odzdvds  13053  pcdvdsb  13128  lgsne0  16362  lgsquadlem3  16403  bj-nnor  16967