Theorem imnan 261

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 242	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2	1	con2bii 238	1 |- ((ph -> -. ps) <-> -. (ph /\ ps))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  pm4.15 380  anass 487  pm5.18OLD 723  pm5.17 731  dfbi3 733  nan 753  ecase2d 824  nic-ax 1239  nic-axALT 1240  alinexa 1389  dfsb3 1596  a12lem2 1768  a12study 1769  ralinexa 2143  eueq3 2430  pssn2lp 2709  ssnpssOLD 2713  difinOLD 2832  disj 2914  minel 2929  inssdif0OLD 2941  disjsn 3089  sotric 3615  fr0 3636  ordtri1 3693  ordtri1OLD 3694  dfwe2OLD 3862  ordsucss 3899  onuninsuci 3921  ordunisuc2 3926  funun 4462  imadif 4493  oalimcl 5242  omlimcl 5257  unblem1 5633  suppr 5680  ordiso 5683  kmlem4 5930  alephnbtwn 6016  alephsucpw 6018  alephsucdom 6028  cfsuc 6063  genpnnp 6260  ltnsym2OLD 6704  xrltnsym2 6726  nneoi 7409  sqr2irrlem3 7976  aleph1re 8820  clsval2 8961  ntreq0 8984  bcthlem7 9283  nmounbi 9778  pilem1 10020  fsubbas 10281  fbunfip 10282  cvnsym 11862  hatomistici 11934  bnj1215 12991  bnj1305 13048  bnj1474 13151  bnj1533 13182  bnj1284 13482  poseq 13954  axdenselem5 14023  axdenselem7 14025  nocvxminlem 14028  df3nandALT1 14146  df3nandALT2 14147  cnfilca 14927  ordisoOLD 15374  fbasfip 15556  filssufillem 15570  fixufil 15576  rnelfmlem 15592  flimfnfcls 15615  nninfnub 15819  n0el 16248  pm10.57 16318  strdif 16719  pltn2lp 16789  hlatmstc 17047

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 164  df-an 242

Copyright terms: Public domain