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

Theorem biimprd 147
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 145 1 (φ → (χψ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  syl6bir  153  mpbird  156  sylibrd  158  sylbird  159  imbi1d  220  biimpar  281  notbid  591  mtbid  596  mtbii  598  orbi2d  703  pm4.55dc  845  pm3.11dc  863  prlem1  879  nfimd  1474  dral1  1615  cbvalh  1633  ax16i  1735  speiv  1739  a16g  1741  cleqh  2134  pm13.18  2280  rspcimdv  2651  rspcimedv  2652  rspcedv  2654  moi2  2716  moi  2718  eqrd  2957  ralxfrd  4160  ralxfr2d  4162  rexxfr2d  4163  elres  4589  2elresin  4953  f1ocnv  5082  tz6.12c  5146  fvun1  5182  dffo4  5258  isores3  5398  tposfo2  5823  issmo2  5845  iordsmo  5853  smoel2  5859  prarloclemarch  6401  genprndl  6503  genprndu  6504  ltpopr  6568  ltsopr  6569  recexprlem1ssl  6604  recexprlem1ssu  6605  aptiprlemu  6611  lttrsr  6670  nnmulcl  7696  nnnegz  8004  eluzdc  8303  negm  8306  iccid  8544  icoshft  8608  fzen  8657  elfz2nn0  8723  elfzom1p1elfzo  8820  bj-omssind  9369  bj-bdfindes  9383  bj-nntrans  9385  bj-nnelirr  9387  bj-omtrans  9390  setindis  9397  bdsetindis  9399  bj-inf2vnlem3  9402  bj-inf2vnlem4  9403  bj-findis  9409  bj-findes  9411
  Copyright terms: Public domain W3C validator