ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimprd Structured version   Unicode version

Theorem biimprd 147
Description: Deduce a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
Hypothesis
Ref Expression
biimprd.1
Assertion
Ref Expression
biimprd

Proof of Theorem biimprd
StepHypRef Expression
1 id 19 . 2
2 biimprd.1 . 2
31, 2syl5ibr 145 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  syl6bir  153  mpbird  156  sylibrd  158  sylbird  159  imbi1d  220  biimpar  281  notbid  576  mtbid  581  mtbii  583  orbi2d  688  pm4.55dc  828  pm3.11dc  846  prlem1  862  nfimd  1450  dral1  1591  cbvalh  1609  ax16i  1711  speiv  1715  a16g  1717  cleqh  2110  pm13.18  2255  rspcimdv  2625  rspcimedv  2626  rspcedv  2628  moi2  2690  moi  2692  eqrd  2931  ralxfrd  4132  ralxfr2d  4134  rexxfr2d  4135  elres  4561  2elresin  4924  f1ocnv  5052  tz6.12c  5116  fvun1  5152  dffo4  5228  isores3  5368  tposfo2  5792  issmo2  5814  iordsmo  5822  smoel2  5828  prarloclemarch  6261  genprndl  6362  genprndu  6363  ltpopr  6418  ltsopr  6419  recexprlem1ssl  6454  recexprlem1ssu  6455  aptiprlemu  6461  lttrsr  6500  nnmulcl  7518  nnnegz  7822  bj-omssind  8319  bj-bdfindes  8333  bj-nntrans  8335  bj-nnelirr  8337  bj-omtrans  8340  setindis  8347  bdsetindis  8349  bj-inf2vnlem3  8352  bj-inf2vnlem4  8353  bj-findis  8359  bj-findes  8361
  Copyright terms: Public domain W3C validator