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 660  pm5.17 668  dfbi3 670  nan 689  ecase2d 751  nicodraw 952  alinexa 1042  dfsb3 1226  a12lem2 1377  a12study 1378  ralinexa 1683  eueq3 1919  ssnpss 2149  difin 2245  disj 2311  minel 2324  inssdif0 2333  sotric 2860  fr0 2927  dfwe2 2935  ordtri1 2980  ordsucss 3069  onuninsuc 3108  ordunisuc2 3115  funun 3554  imadif 3574  oalimcl 4194  omlimcl 4209  0nelqs 4298  unblem1 4540  suppr 4590  kmlem4 4768  alephnbtwn 4868  alephsucpw 4870  alephsucdom 4880  cfsuc 4915  genpnnp 5108  ltnsym2t 5533  xrltnsym2t 5551  nneo 6197  sqr2irrlem3 6726  aleph1re 7551  clsval2 7685  ntreq0 7708  bcthlem7 8005  nmounbi 8439  pilem1 8671  cvnsymt 10217  hatomistic 10289  cnfilca 10583  cnfilcaOLD 10584

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