Theorem imnan 623

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 565	. . . 4 |- (ph -> (ps -> -. (ph -> -. ps)))
2	1	imp 115	. . 3 |- ((ph /\ ps) -> -. (ph -> -. ps))
3	2	con2i 557	. 2 |- ((ph -> -. ps) -> -. (ph /\ ps))
4		pm3.2 126	. . 3 |- (ph -> (ps -> (ph /\ ps)))
5	4	con3rr3 562	. 2 |- (-. (ph /\ ps) -> (ph -> -. ps))
6	3, 5	impbii 117	1 |- ((ph -> -. ps) <-> -. (ph /\ ps))

Syntax hints:  -. wn 3   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  imnani  624  nan  625  pm3.24  626  imandc  785  ianordc  798  pm5.17dc  809  dn1dc  866  xorbin  1272  xordc1  1281  mpto1  1311  alinexa  1491  ralinexa  2345  pssn2lp  3039  rabeq0  3241  disj  3262  minel  3277  disjsn  3423  sotricim  4051  poirr2  4660  funun  4887  imadiflem  4921  imadif  4922  brprcneu  5114  prltlu  6470  caucvgprlemnbj  6638  xrltnsym2  8485  fzp1nel  8736