Theorem imnan 697

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 642	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 124	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3	2	con2i 632	. 2 |- ( ( ph -> -. ps ) -> -. ( ph /\ ps ) )
4		pm3.2 139	. . 3 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
5	4	con3rr3 638	. 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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imnani  698  nan  699  mpnanrd  700  pm3.24  701  imanst  896  ianordc  907  pm5.17dc  912  dn1dc  969  xorbin  1429  xordc1  1438  alinexa  1652  dfrex2dc  2524  ralinexa  2560  rabeq0  3526  disj  3545  minel  3558  disjsn  3735  sotricim  4426  poirr2  5136  funun  5378  imadiflem  5416  imadif  5417  brprcneu  5641  2omotaplemap  7536  prltlu  7767  caucvgprlemnbj  7947  caucvgprprlemnbj  7973  suplocexprlemmu  7998  xrltnsym2  10090  fzp1nel  10401  fsumsplit  12048  sumsplitdc  12073  phiprmpw  12874  odzdvds  12898  pcdvdsb  12973  lgsne0  15857  lgsquadlem3  15898  bj-nnor  16452