Theorem imnan 691

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  692  nan  693  pm3.24  694  imanst  889  ianordc  900  pm5.17dc  905  dn1dc  962  xorbin  1395  xordc1  1404  alinexa  1617  dfrex2dc  2488  ralinexa  2524  rabeq0  3480  disj  3499  minel  3512  disjsn  3684  sotricim  4358  poirr2  5062  funun  5302  imadiflem  5337  imadif  5338  brprcneu  5551  2omotaplemap  7324  prltlu  7554  caucvgprlemnbj  7734  caucvgprprlemnbj  7760  suplocexprlemmu  7785  xrltnsym2  9869  fzp1nel  10179  fsumsplit  11572  sumsplitdc  11597  phiprmpw  12390  odzdvds  12414  pcdvdsb  12489  lgsne0  15279  lgsquadlem3  15320  bj-nnor  15380