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  6516  genprndl  6619  genprndu  6620  ltpopr  6693  ltsopr  6694  recexprlem1ssl  6731  recexprlem1ssu  6732  aptiprlemu  6738  lttrsr  6847  nnmulcl  7935  nnnegz  8248  eluzdc  8547  negm  8550  iccid  8794  icoshft  8858  fzen  8907  elfz2nn0  8973  elfzom1p1elfzo  9070  flqeqceilz  9160  caucvgre  9580  qdenre  9798  ialginv  9886  ialgfx  9891  bj-omssind  10059  bj-bdfindes  10074  bj-nntrans  10076  bj-nnelirr  10078  bj-omtrans  10081  setindis  10092  bdsetindis  10094  bj-inf2vnlem3  10097  bj-inf2vnlem4  10098  bj-findis  10104  bj-findes  10106
 Copyright terms: Public domain W3C validator