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

Theorem biimprd 157
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 155 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  syl6bir  163  mpbird  166  sylibrd  168  sylbird  169  imbi1d  230  biimpar  295  mtbid  662  mtbii  664  orbi2d  780  pm4.55dc  923  pm3.11dc  942  prlem1  958  nfimd  1565  dral1  1709  cbvalh  1727  ax16i  1831  speiv  1835  a16g  1837  cleqh  2240  pm13.18  2390  rspcimdv  2793  rspcimedv  2794  rspcedv  2796  moi2  2868  moi  2870  eqrd  3119  abnexg  4374  ralxfrd  4390  ralxfr2d  4392  rexxfr2d  4393  elres  4862  2elresin  5241  f1ocnv  5387  tz6.12c  5458  fvun1  5494  dffo4  5575  isores3  5723  tposfo2  6171  issmo2  6193  iordsmo  6201  smoel2  6207  fiintim  6824  ismkvnex  7036  prarloclemarch  7249  genprndl  7352  genprndu  7353  ltpopr  7426  ltsopr  7427  recexprlem1ssl  7464  recexprlem1ssu  7465  aptiprlemu  7471  lttrsr  7593  nnmulcl  8764  nnnegz  9080  eluzdc  9430  negm  9433  iccid  9737  icoshft  9802  fzen  9853  elfz2nn0  9922  elfzom1p1elfzo  10021  flqeqceilz  10121  zmodidfzoimp  10157  caucvgre  10784  qdenre  11005  dvdsval2  11530  negdvdsb  11543  muldvds2  11553  dvdsabseq  11579  bezoutlemaz  11725  bezoutlembz  11726  rplpwr  11749  alginv  11762  algfx  11767  coprmgcdb  11803  divgcdcoprm0  11816  prmgt1  11846  oddprmgt2  11848  rpexp1i  11866  2sqpwodd  11888  qnumdencl  11899  phiprmpw  11932  oddennn  11939  cnpnei  12425  bl2in  12609  addcncntoplem  12757  rescncf  12774  limcresi  12841  cnplimcim  12842  efltlemlt  12901  ioocosf1o  12981  uzdcinzz  13174  bj-omssind  13302  bj-bdfindes  13316  bj-nntrans  13318  bj-nnelirr  13320  bj-omtrans  13323  setindis  13334  bdsetindis  13336  bj-inf2vnlem3  13339  bj-inf2vnlem4  13340  bj-findis  13346  bj-findes  13348
  Copyright terms: Public domain W3C validator