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  1614  dfrex2dc  2485  ralinexa  2521  rabeq0  3476  disj  3495  minel  3508  disjsn  3680  sotricim  4354  poirr2  5058  funun  5298  imadiflem  5333  imadif  5334  brprcneu  5547  2omotaplemap  7317  prltlu  7547  caucvgprlemnbj  7727  caucvgprprlemnbj  7753  suplocexprlemmu  7778  xrltnsym2  9860  fzp1nel  10170  fsumsplit  11550  sumsplitdc  11575  phiprmpw  12360  odzdvds  12383  pcdvdsb  12458  lgsne0  15154  bj-nnor  15226