Theorem imnan 701

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 646	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 124	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3	2	con2i 636	. 2 |- ( ( ph -> -. ps ) -> -. ( ph /\ ps ) )
4		pm3.2 139	. . 3 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
5	4	con3rr3 642	. 2 |- ( -. ( ph /\ ps ) -> ( ph -> -. ps ) )
6	3, 5	impbii 126	1 |- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  imnani  702  nan  703  mpnanrd  704  pm3.24  705  imanst  900  ianordc  911  pm5.17dc  916  dn1dc  973  xorbin  1433  xordc1  1442  alinexa  1656  dfrex2dc  2541  ralinexa  2577  rabeq0  3552  disj  3573  minel  3586  disjsn  3771  sotricim  4468  poirr2  5180  funun  5422  imadiflem  5460  imadif  5461  brprcneu  5688  2omotaplemap  7623  prltlu  7854  caucvgprlemnbj  8034  caucvgprprlemnbj  8060  suplocexprlemmu  8085  xrltnsym2  10196  fzp1nel  10511  fsumsplit  12174  sumsplitdc  12199  phiprmpw  13000  odzdvds  13024  pcdvdsb  13099  lgsne0  16157  lgsquadlem3  16198  bj-nnor  16762