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

Theorem biimprcd 158
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 155 1 (𝜒 → (𝜑𝜓))
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:  biimparc  293  pm5.32  441  oplem1  921  ax11i  1649  equsex  1663  eleq1a  2159  ceqsalg  2647  cgsexg  2654  cgsex2g  2655  cgsex4g  2656  ceqsex  2657  spc2egv  2708  spc3egv  2710  csbiebt  2967  dfiin2g  3763  sotricim  4150  ralxfrALT  4289  iunpw  4302  opelxp  4467  ssrel  4526  ssrel2  4528  ssrelrel  4538  iss  4758  funcnvuni  5083  fun11iun  5274  tfrlem8  6083  eroveu  6381  fundmen  6521  nneneq  6571  fidifsnen  6584  prarloclem5  7057  prarloc  7060  recexprlemss1l  7192  recexprlemss1u  7193  uzin  9049  indstr  9079  elfzmlbp  9539
  Copyright terms: Public domain W3C validator