Theorem imnan 242

Description: Express implication in terms of conjunction.

Assertion

Ref	Expression
imnan	|- ((ph -> -. ps) <-> -. (ph /\ ps))

Proof of Theorem imnan

Step	Hyp	Ref	Expression
1		df-an 225	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2	1	con2bii 221	1 |- ((ph -> -. ps) <-> -. (ph /\ ps))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm4.15 353  anass 439  pm5.18 658  pm5.17 666  dfbi 668  nan 687  ecase2d 749  nicodraw 949  alinexa 1038  dfsb3 1221  a12lem2 1370  a12study 1371  ralinexa 1675  eueq3 1910  ssnpss 2139  difin 2235  disj 2301  minel 2314  inssdif0 2323  sotric 2851  fr0 2917  dfwe2 2925  ordtri1 2970  ordsucss 3059  onuninsuc 3098  ordunisuc2 3105  funun 3540  imadif 3560  oalimcl 4178  omlimcl 4193  0nelqs 4282  unblem1 4517  suppr 4562  kmlem4 4740  alephnbtwn 4840  alephsucpw 4842  alephsucdom 4852  cfsuc 4887  genpnnp 5080  ltnsym2t 5506  xrltnsym2t 5524  nneo 6144  sqr2irrlem3 6656  aleph1re 7494  clsval2 7627  ntreq0 7650  bcthlem7 7939  nmounbi 8371  pilem1 8590  cvnsymt 10127  hatomistic 10197  cnfilca 10451

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain