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

Theorem biimpr 220
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
Assertion
Ref Expression
biimpr ((𝜑𝜓) → (𝜓𝜑))

Proof of Theorem biimpr
StepHypRef Expression
1 dfbi1 213 . 2 ((𝜑𝜓) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
2 simprim 166 . 2 (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜓𝜑))
31, 2sylbi 217 1 ((𝜑𝜓) → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206
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 207
This theorem is referenced by:  bicom1  221  pm5.74  270  bija  380  simplbi2comt  501  pm4.72  951  bianir  1058  albi  1819  spsbbi  2078  cbv2w  2339  cbv2  2405  cbv2h  2408  equvel  2458  dfeumo  2534  eu6  2572  2eu6  2655  ralbi  3089  rexbi  3090  ceqsal1t  3471  elabgtOLD  3625  elabgtOLDOLD  3626  euind  3680  reu6  3682  reuind  3709  sbciegftOLD  3776  sepex  5243  axprALT  5365  axprOLD  5374  iota4  6471  fv3  6850  elirrv  9500  r1omhfb  35217  fineqvpow  35220  r1omhfbregs  35242  nn0prpwlem  36465  nn0prpw  36466  bj-animbi  36702  bj-bi3ant  36732  bj-cbv2hv  36941  bj-ceqsalt0  37028  bj-ceqsalt1  37029  bj-bm1.3ii  37208  dfgcd3  37468  tsbi3  38275  mapdrvallem2  41844  eu6w  42861  axc11next  44589  pm13.192  44593  exbir  44662  con5  44705  sbcim2g  44721  trsspwALT  45000  trsspwALT2  45001  sspwtr  45003  sspwtrALT  45004  pwtrVD  45006  pwtrrVD  45007  snssiALTVD  45009  sstrALT2VD  45016  sstrALT2  45017  suctrALT2VD  45018  eqsbc2VD  45022  simplbi2VD  45028  exbirVD  45035  exbiriVD  45036  imbi12VD  45055  sbcim2gVD  45057  simplbi2comtVD  45070  con5VD  45082  2uasbanhVD  45093  nimnbi2  45350  absnsb  47215  thincciso  49640
  Copyright terms: Public domain W3C validator