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

Theorem biimprcd 149
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 146 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:  biimparc  283  pm5.32  426  oplem1  881  ax11i  1599  equsex  1613  eleq1a  2106  ceqsalg  2576  cgsexg  2583  cgsex2g  2584  cgsex4g  2585  ceqsex  2586  spc2egv  2636  spc3egv  2638  csbiebt  2880  dfiin2g  3681  sotricim  4051  ralxfrALT  4165  iunpw  4177  opelxp  4317  ssrel  4371  ssrel2  4373  ssrelrel  4383  iss  4597  funcnvuni  4911  fun11iun  5090  tfrlem8  5875  eroveu  6133  fundmen  6222  prarloclem5  6482  prarloc  6485  recexprlemss1l  6606  recexprlemss1u  6607  uzin  8261  indstr  8292  elfzmlbp  8740
  Copyright terms: Public domain W3C validator