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

Theorem biimprcd 153
Description: Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
Hypothesis
Ref Expression
biimpcd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
biimprcd (𝜒 → (𝜑𝜓))

Proof of Theorem biimprcd
StepHypRef Expression
1 id 19 . 2 (𝜒𝜒)
2 biimpcd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5ibrcom 150 1 (𝜒 → (𝜑𝜓))
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:  biimparc  287  pm5.32  434  oplem1  893  ax11i  1618  equsex  1632  eleq1a  2125  ceqsalg  2599  cgsexg  2606  cgsex2g  2607  cgsex4g  2608  ceqsex  2609  spc2egv  2659  spc3egv  2661  csbiebt  2914  dfiin2g  3718  sotricim  4088  ralxfrALT  4227  iunpw  4239  opelxp  4402  ssrel  4456  ssrel2  4458  ssrelrel  4468  iss  4682  funcnvuni  4996  fun11iun  5175  tfrlem8  5965  eroveu  6228  fundmen  6317  nneneq  6351  fidifsnen  6362  prarloclem5  6656  prarloc  6659  recexprlemss1l  6791  recexprlemss1u  6792  uzin  8601  indstr  8632  elfzmlbp  9092
  Copyright terms: Public domain W3C validator