Theorem imnan 624

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 566	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 115	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3	2	con2i 557	. 2 |- ( ( ph -> -. ps ) -> -. ( ph /\ ps ) )
4		pm3.2 126	. . 3 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
5	4	con3rr3 563	. 2 |- ( -. ( ph /\ ps ) -> ( ph -> -. ps ) )
6	3, 5	impbii 117	1 |- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  imnani  625  nan  626  pm3.24  627  imandc  786  ianordc  799  pm5.17dc  810  dn1dc  867  xorbin  1275  xordc1  1284  alinexa  1494  ralinexa  2351  pssn2lp  3045  rabeq0  3247  disj  3268  minel  3283  disjsn  3432  sotricim  4060  poirr2  4717  funun  4944  imadiflem  4978  imadif  4979  brprcneu  5171  prltlu  6585  caucvgprlemnbj  6765  caucvgprprlemnbj  6791  xrltnsym2  8715  fzp1nel  8966