Theorem imnan 679

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 626	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 123	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3	2	con2i 616	. 2 |- ( ( ph -> -. ps ) -> -. ( ph /\ ps ) )
4		pm3.2 138	. . 3 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
5	4	con3rr3 622	. 2 |- ( -. ( ph /\ ps ) -> ( ph -> -. ps ) )
6	3, 5	impbii 125	1 |- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imnani  680  nan  681  pm3.24  682  imanst  873  ianordc  884  pm5.17dc  889  dn1dc  944  xorbin  1362  xordc1  1371  alinexa  1582  dfrex2dc  2428  ralinexa  2462  rabeq0  3392  disj  3411  minel  3424  disjsn  3585  sotricim  4245  poirr2  4931  funun  5167  imadiflem  5202  imadif  5203  brprcneu  5414  prltlu  7295  caucvgprlemnbj  7475  caucvgprprlemnbj  7501  suplocexprlemmu  7526  xrltnsym2  9580  fzp1nel  9884  fsumsplit  11176  sumsplitdc  11201  phiprmpw  11898  bj-nnor  12946