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

Theorem imnan 411
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
StepHypRef Expression
1 df-an 360 . 2  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
21con2bii 322 1  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  imnani  412  iman  413  ianor  474  nan  563  pm5.17  858  pm5.16  860  dn1  932  nic-ax  1428  nic-axALT  1429  alinexa  1568  dfsb3  2009  ralinexa  2601  pssn2lp  3290  disj  3508  minel  3523  disjsn  3706  sotric  4356  ordtri1  4441  ordsucss  4625  ordunisuc2  4651  poirr2  5083  funun  5312  imadif  5343  brprcneu  5534  soisoi  5841  oalimcl  6574  omlimcl  6592  unblem1  7125  suppr  7235  cantnfp1lem3  7398  alephnbtwn  7714  kmlem4  7795  cfsuc  7899  isf32lem5  7999  hargch  8315  xrltnsym2  10488  fsumsplit  12228  sumsplit  12247  phiprmpw  12860  odzdvds  12876  pcdvdsb  12937  prmreclem5  12983  ramlb  13082  pltn2lp  14119  gsumzsplit  15222  dprdcntz2  15289  lbsextlem4  15930  obselocv  16644  lmmo  17124  kqcldsat  17440  rnelfmlem  17663  tsmssplit  17850  itg2splitlem  19119  itg2split  19120  fsumharmonic  20321  lgsne0  20588  lgsquadlem3  20611  nmounbi  21370  hatomistici  22958  ballotlemfrcn0  23104  eliccelico  23285  elicoelioo  23286  subfacp1lem6  23731  poseq  24324  nodenselem5  24410  nodenselem7  24412  nocvxminlem  24415  nofulllem5  24431  df3nandALT1  24907  df3nandALT2  24908  limsucncmpi  24956  nninfnub  26564  n0el  26828  fnwe2lem2  27251  pm10.57  27669  stoweidlem14  27866  stoweidlem34  27886  stoweidlem44  27896  bnj1533  29200  bnj1204  29358  bnj1280  29366  dfsb3NEW7  29610  a12lem2  29753  a12study  29754  a12study10  29758  a12study10n  29759  atlatmstc  30131
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator