Theorem imnan 438

Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.)

Assertion

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

Proof of Theorem imnan

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384

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

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  imnani  439  iman  440  ianor  509  nan  604  pm5.17  932  pm5.16  934  dn1  1008  nannan  1451  nic-ax  1598  nic-axALT  1599  imnang  1769  dfsb3  2374  ralinexa  2997  pssn2lp  3708  disj  4017  minelOLD  4034  disjsn  4246  sotric  5061  poirr2  5520  ordtri1  5756  funun  5932  imadif  5973  brprcneu  6184  soisoi  6578  ordsucss  7018  ordunisuc2  7044  oalimcl  7640  omlimcl  7658  unblem1  8212  suppr  8377  infpr  8409  cantnfp1lem3  8577  alephnbtwn  8894  kmlem4  8975  cfsuc  9079  isf32lem5  9179  hargch  9495  xrltnsym2  11971  fzp1nel  12424  fsumsplit  14471  sumsplit  14499  phiprmpw  15481  odzdvds  15500  pcdvdsb  15573  prmreclem5  15624  ramlb  15723  pltn2lp  16969  gsumzsplit  18327  dprdcntz2  18437  lbsextlem4  19161  obselocv  20072  maducoeval2  20446  lmmo  21184  kqcldsat  21536  rnelfmlem  21756  tsmssplit  21955  itg2splitlem  23515  itg2split  23516  fsumharmonic  24738  lgsne0  25060  lgsquadlem3  25107  axtgupdim2  25370  nmounbi  27631  hatomistici  29221  eliccelico  29539  elicoelioo  29540  nn0min  29567  2sqcoprm  29647  isarchi2  29739  archiabl  29752  oddpwdc  30416  eulerpartlemsv2  30420  eulerpartlems  30422  eulerpartlemv  30426  eulerpartlemgh  30440  eulerpartlemgs2  30442  ballotlemfrcn0  30591  bnj1533  30922  bnj1204  31080  bnj1280  31088  subfacp1lem6  31167  poseq  31750  wzel  31771  wzelOLD  31772  nosepssdm  31836  nosupbnd1lem4  31857  nocvxminlem  31893  df3nandALT1  32396  df3nandALT2  32397  limsucncmpi  32444  unblimceq0  32498  mpnanrd  33178  relowlpssretop  33212  wl-dfnan2  33296  nninfnub  33547  atlatmstc  34606  fnwe2lem2  37621  dfxor4  38058  pm10.57  38570  limclner  39883  limsupub  39936  limsuppnflem  39942  limsupre2lem  39956  icccncfext  40100  stoweidlem14  40231  stoweidlem34  40251  stoweidlem44  40261  ldepslinc  42298  elsetrecslem  42444  alimp-no-surprise  42527