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 657  pm5.17 665  dfbi 667  nan 686  ecase2d 748  nicodraw 948  alinexa 1018  dfsb3 1210  a12lem2 1354  a12study 1355  ralinexa 1659  eueq3 1891  ssnpss 2120  difin 2216  disj 2282  minel 2295  inssdif0 2304  sotric 2824  fr0 2890  dfwe2 2898  ordtri1 2943  ordsucss 3032  onuninsuc 3071  ordunisuc2 3078  funun 3494  imadif 3514  oalimcl 4132  omlimcl 4147  0nelqs 4236  unblem1 4469  suppr 4514  kmlem4 4692  alephnbtwn 4791  alephsucpw 4793  alephsucdom 4803  cfsuc 4838  genpnnp 5031  ltnsym2t 5457  xrltnsym2t 5475  nneo 6095  sqr2irrlem3 6607  aleph1re 7445  clsval2 7578  ntreq0 7599  bcthlem7 7887  nmounbi 8306  pilem1 8503  cnfilca 8801  cvnsymt 10341  hatomistic 10411

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