ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimprd Unicode 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  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimprd  |-  ( ph  ->  ( ch  ->  ps ) )

Proof of Theorem biimprd
StepHypRef Expression
1 id 19 . 2  |-  ( ch 
->  ch )
2 biimprd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibr 154 1  |-  ( ph  ->  ( ch  ->  ps ) )
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  4257  ralxfr2d  4259  rexxfr2d  4260  elres  4714  2elresin  5087  f1ocnv  5223  tz6.12c  5291  fvun1  5327  dffo4  5404  isores3  5549  tposfo2  5980  issmo2  6002  iordsmo  6010  smoel2  6016  prarloclemarch  6914  genprndl  7017  genprndu  7018  ltpopr  7091  ltsopr  7092  recexprlem1ssl  7129  recexprlem1ssu  7130  aptiprlemu  7136  lttrsr  7245  nnmulcl  8371  nnnegz  8679  eluzdc  9022  negm  9025  iccid  9268  icoshft  9332  fzen  9382  elfz2nn0  9449  elfzom1p1elfzo  9546  flqeqceilz  9646  zmodidfzoimp  9682  caucvgre  10302  qdenre  10523  dvdsval2  10666  negdvdsb  10679  muldvds2  10689  dvdsabseq  10715  bezoutlemaz  10859  bezoutlembz  10860  rplpwr  10883  ialginv  10896  ialgfx  10901  coprmgcdb  10937  divgcdcoprm0  10950  prmgt1  10980  oddprmgt2  10982  rpexp1i  11000  2sqpwodd  11021  qnumdencl  11032  phiprmpw  11065  oddennn  11072  uzdcinzz  11128  bj-omssind  11260  bj-bdfindes  11274  bj-nntrans  11276  bj-nnelirr  11278  bj-omtrans  11281  setindis  11292  bdsetindis  11294  bj-inf2vnlem3  11297  bj-inf2vnlem4  11298  bj-findis  11304  bj-findes  11306
  Copyright terms: Public domain W3C validator