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

Theorem biimprd 156
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 154 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  syl6bir  162  mpbird  165  sylibrd  167  sylbird  168  imbi1d  229  biimpar  291  notbid  625  mtbid  630  mtbii  632  orbi2d  737  pm4.55dc  882  pm3.11dc  901  prlem1  917  nfimd  1520  dral1  1662  cbvalh  1680  ax16i  1783  speiv  1787  a16g  1789  cleqh  2184  pm13.18  2332  rspcimdv  2716  rspcimedv  2717  rspcedv  2719  moi2  2787  moi  2789  eqrd  3032  ralxfrd  4258  ralxfr2d  4260  rexxfr2d  4261  elres  4715  2elresin  5090  f1ocnv  5229  tz6.12c  5297  fvun1  5333  dffo4  5410  isores3  5555  tposfo2  5986  issmo2  6008  iordsmo  6016  smoel2  6022  prarloclemarch  6921  genprndl  7024  genprndu  7025  ltpopr  7098  ltsopr  7099  recexprlem1ssl  7136  recexprlem1ssu  7137  aptiprlemu  7143  lttrsr  7252  nnmulcl  8378  nnnegz  8686  eluzdc  9029  negm  9032  iccid  9275  icoshft  9339  fzen  9389  elfz2nn0  9456  elfzom1p1elfzo  9553  flqeqceilz  9653  zmodidfzoimp  9689  caucvgre  10310  qdenre  10531  dvdsval2  10681  negdvdsb  10694  muldvds2  10704  dvdsabseq  10730  bezoutlemaz  10874  bezoutlembz  10875  rplpwr  10898  ialginv  10911  ialgfx  10916  coprmgcdb  10952  divgcdcoprm0  10965  prmgt1  10995  oddprmgt2  10997  rpexp1i  11015  2sqpwodd  11036  qnumdencl  11047  phiprmpw  11080  oddennn  11087  uzdcinzz  11143  bj-omssind  11275  bj-bdfindes  11289  bj-nntrans  11291  bj-nnelirr  11293  bj-omtrans  11296  setindis  11307  bdsetindis  11309  bj-inf2vnlem3  11312  bj-inf2vnlem4  11313  bj-findis  11319  bj-findes  11321
  Copyright terms: Public domain W3C validator