Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imnan Structured version   Visualization version   GIF version

Theorem imnan 437
 Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.)
Assertion
Ref Expression
imnan ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))

Proof of Theorem imnan
StepHypRef Expression
1 df-an 385 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
21con2bii 346 1 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383 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 385 This theorem is referenced by:  imnani  438  iman  439  ianor  510  nan  605  pm5.17  968  pm5.16  970  dn1  1046  nannan  1600  nic-ax  1747  nic-axALT  1748  imnang  1918  dfsb3  2511  ralinexa  3135  pssn2lp  3850  disj  4160  minelOLD  4178  disjsn  4390  sotric  5213  poirr2  5678  ordtri1  5917  funun  6093  imadif  6134  brprcneu  6345  soisoi  6741  ordsucss  7183  ordunisuc2  7209  oalimcl  7809  omlimcl  7827  unblem1  8377  suppr  8542  infpr  8574  cantnfp1lem3  8750  alephnbtwn  9084  kmlem4  9167  cfsuc  9271  isf32lem5  9371  hargch  9687  xrltnsym2  12164  fzp1nel  12617  fsumsplit  14670  sumsplit  14698  phiprmpw  15683  odzdvds  15702  pcdvdsb  15775  prmreclem5  15826  ramlb  15925  pltn2lp  17170  gsumzsplit  18527  dprdcntz2  18637  lbsextlem4  19363  obselocv  20274  maducoeval2  20648  lmmo  21386  kqcldsat  21738  rnelfmlem  21957  tsmssplit  22156  itg2splitlem  23714  itg2split  23715  fsumharmonic  24937  lgsne0  25259  lgsquadlem3  25306  axtgupdim2  25569  nmounbi  27940  hatomistici  29530  eliccelico  29848  elicoelioo  29849  nn0min  29876  2sqcoprm  29956  isarchi2  30048  archiabl  30061  oddpwdc  30725  eulerpartlemsv2  30729  eulerpartlems  30731  eulerpartlemv  30735  eulerpartlemgh  30749  eulerpartlemgs2  30751  ballotlemfrcn0  30900  bnj1533  31229  bnj1204  31387  bnj1280  31395  subfacp1lem6  31474  poseq  32059  wzel  32075  nosepssdm  32142  nosupbnd1lem4  32163  nocvxminlem  32199  df3nandALT1  32702  df3nandALT2  32703  limsucncmpi  32750  unblimceq0  32804  mpnanrd  33489  relowlpssretop  33523  wl-dfnan2  33609  nninfnub  33860  atlatmstc  35109  fnwe2lem2  38123  dfxor4  38560  pm10.57  39072  limclner  40386  limsupub  40439  limsuppnflem  40445  limsupre2lem  40459  icccncfext  40603  stoweidlem14  40734  stoweidlem34  40754  stoweidlem44  40764  ldepslinc  42808  elsetrecslem  42955  alimp-no-surprise  43040
 Copyright terms: Public domain W3C validator