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

Theorem biimprd 151
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 149 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  syl6bir  157  mpbird  160  sylibrd  162  sylbird  163  imbi1d  224  biimpar  285  notbid  602  mtbid  607  mtbii  609  orbi2d  714  pm4.55dc  857  pm3.11dc  875  prlem1  891  nfimd  1493  dral1  1634  cbvalh  1652  ax16i  1754  speiv  1758  a16g  1760  cleqh  2153  pm13.18  2301  rspcimdv  2674  rspcimedv  2675  rspcedv  2677  moi2  2745  moi  2747  eqrd  2991  ralxfrd  4222  ralxfr2d  4224  rexxfr2d  4225  elres  4674  2elresin  5038  f1ocnv  5167  tz6.12c  5231  fvun1  5267  dffo4  5343  isores3  5483  tposfo2  5913  issmo2  5935  iordsmo  5943  smoel2  5949  prarloclemarch  6574  genprndl  6677  genprndu  6678  ltpopr  6751  ltsopr  6752  recexprlem1ssl  6789  recexprlem1ssu  6790  aptiprlemu  6796  lttrsr  6905  nnmulcl  8011  nnnegz  8305  eluzdc  8644  negm  8647  iccid  8895  icoshft  8959  fzen  9009  elfz2nn0  9075  elfzom1p1elfzo  9172  flqeqceilz  9268  zmodidfzoimp  9304  caucvgre  9808  qdenre  10029  dvdsval2  10111  negdvdsb  10124  muldvds2  10133  dvdsabseq  10159  ialginv  10269  ialgfx  10274  bj-omssind  10446  bj-bdfindes  10461  bj-nntrans  10463  bj-nnelirr  10465  bj-omtrans  10468  setindis  10479  bdsetindis  10481  bj-inf2vnlem3  10484  bj-inf2vnlem4  10485  bj-findis  10491  bj-findes  10493
  Copyright terms: Public domain W3C validator