ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimprd GIF 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  592  mtbid  597  mtbii  599  orbi2d  704  pm4.55dc  846  pm3.11dc  864  prlem1  880  nfimd  1477  dral1  1618  cbvalh  1636  ax16i  1738  speiv  1742  a16g  1744  cleqh  2137  pm13.18  2286  rspcimdv  2657  rspcimedv  2658  rspcedv  2660  moi2  2722  moi  2724  eqrd  2963  ralxfrd  4194  ralxfr2d  4196  rexxfr2d  4197  elres  4646  2elresin  5010  f1ocnv  5139  tz6.12c  5203  fvun1  5239  dffo4  5315  isores3  5455  tposfo2  5882  issmo2  5904  iordsmo  5912  smoel2  5918  prarloclemarch  6514  genprndl  6617  genprndu  6618  ltpopr  6691  ltsopr  6692  recexprlem1ssl  6729  recexprlem1ssu  6730  aptiprlemu  6736  lttrsr  6845  nnmulcl  7933  nnnegz  8246  eluzdc  8545  negm  8548  iccid  8792  icoshft  8856  fzen  8905  elfz2nn0  8971  elfzom1p1elfzo  9068  flqeqceilz  9158  caucvgre  9578  qdenre  9796  ialginv  9884  ialgfx  9889  bj-omssind  10057  bj-bdfindes  10072  bj-nntrans  10074  bj-nnelirr  10076  bj-omtrans  10079  setindis  10090  bdsetindis  10092  bj-inf2vnlem3  10095  bj-inf2vnlem4  10096  bj-findis  10102  bj-findes  10104
  Copyright terms: Public domain W3C validator