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  880  pm3.11dc  899  prlem1  915  nfimd  1518  dral1  1659  cbvalh  1677  ax16i  1780  speiv  1784  a16g  1786  cleqh  2179  pm13.18  2327  rspcimdv  2703  rspcimedv  2704  rspcedv  2706  moi2  2774  moi  2776  eqrd  3018  ralxfrd  4220  ralxfr2d  4222  rexxfr2d  4223  elres  4674  2elresin  5041  f1ocnv  5170  tz6.12c  5235  fvun1  5271  dffo4  5347  isores3  5486  tposfo2  5916  issmo2  5938  iordsmo  5946  smoel2  5952  prarloclemarch  6670  genprndl  6773  genprndu  6774  ltpopr  6847  ltsopr  6848  recexprlem1ssl  6885  recexprlem1ssu  6886  aptiprlemu  6892  lttrsr  7001  nnmulcl  8127  nnnegz  8435  eluzdc  8778  negm  8781  iccid  9024  icoshft  9088  fzen  9138  elfz2nn0  9205  elfzom1p1elfzo  9300  flqeqceilz  9400  zmodidfzoimp  9436  caucvgre  10005  qdenre  10226  dvdsval2  10343  negdvdsb  10356  muldvds2  10366  dvdsabseq  10392  bezoutlemaz  10536  bezoutlembz  10537  rplpwr  10560  ialginv  10573  ialgfx  10578  coprmgcdb  10614  divgcdcoprm0  10627  prmgt1  10657  oddprmgt2  10659  rpexp1i  10677  2sqpwodd  10698  oddennn  10703  uzdcinzz  10759  bj-omssind  10888  bj-bdfindes  10902  bj-nntrans  10904  bj-nnelirr  10906  bj-omtrans  10909  setindis  10920  bdsetindis  10922  bj-inf2vnlem3  10925  bj-inf2vnlem4  10926  bj-findis  10932  bj-findes  10934
  Copyright terms: Public domain W3C validator