ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimprd Unicode 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  |-  ( 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 155 1  |-  ( ph  ->  ( ch  ->  ps ) )
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  646  mtbii  648  orbi2d  764  pm4.55dc  907  pm3.11dc  926  prlem1  942  nfimd  1549  dral1  1693  cbvalh  1711  ax16i  1814  speiv  1818  a16g  1820  cleqh  2217  pm13.18  2366  rspcimdv  2764  rspcimedv  2765  rspcedv  2767  moi2  2838  moi  2840  eqrd  3085  abnexg  4337  ralxfrd  4353  ralxfr2d  4355  rexxfr2d  4356  elres  4825  2elresin  5204  f1ocnv  5348  tz6.12c  5419  fvun1  5455  dffo4  5536  isores3  5684  tposfo2  6132  issmo2  6154  iordsmo  6162  smoel2  6168  fiintim  6785  ismkvnex  6997  prarloclemarch  7194  genprndl  7297  genprndu  7298  ltpopr  7371  ltsopr  7372  recexprlem1ssl  7409  recexprlem1ssu  7410  aptiprlemu  7416  lttrsr  7538  nnmulcl  8709  nnnegz  9025  eluzdc  9372  negm  9375  iccid  9676  icoshft  9741  fzen  9791  elfz2nn0  9860  elfzom1p1elfzo  9959  flqeqceilz  10059  zmodidfzoimp  10095  caucvgre  10721  qdenre  10942  dvdsval2  11423  negdvdsb  11436  muldvds2  11446  dvdsabseq  11472  bezoutlemaz  11618  bezoutlembz  11619  rplpwr  11642  alginv  11655  algfx  11660  coprmgcdb  11696  divgcdcoprm0  11709  prmgt1  11739  oddprmgt2  11741  rpexp1i  11759  2sqpwodd  11781  qnumdencl  11792  phiprmpw  11825  oddennn  11832  cnpnei  12315  bl2in  12499  addcncntoplem  12647  rescncf  12664  limcresi  12731  cnplimcim  12732  uzdcinzz  12932  bj-omssind  13060  bj-bdfindes  13074  bj-nntrans  13076  bj-nnelirr  13078  bj-omtrans  13081  setindis  13092  bdsetindis  13094  bj-inf2vnlem3  13097  bj-inf2vnlem4  13098  bj-findis  13104  bj-findes  13106
  Copyright terms: Public domain W3C validator