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  7624  prltlu  7855  caucvgprlemnbj  8035  caucvgprprlemnbj  8061  suplocexprlemmu  8086  xrltnsym2  10207  fzp1nel  10522  fsumsplit  12193  sumsplitdc  12218  phiprmpw  13023  odzdvds  13047  pcdvdsb  13122  lgsne0  16323  lgsquadlem3  16364  bj-nnor  16928