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

Theorem biimprcd 160
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 157 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  biimparc  299  pm5.32  453  oplem1  977  ax11i  1725  equsex  1739  eleq1a  2261  ceqsalg  2780  cgsexg  2787  cgsex2g  2788  cgsex4g  2789  ceqsex  2790  spc2egv  2842  spc3egv  2844  csbiebt  3111  dfiin2g  3934  sotricim  4341  ralxfrALT  4485  iunpw  4498  opelxp  4674  ssrel  4732  ssrel2  4734  ssrelrel  4744  iss  4971  funcnvuni  5304  fun11iun  5501  tfrlem8  6344  eroveu  6653  fundmen  6833  nneneq  6886  fidifsnen  6899  prarloclem5  7530  prarloc  7533  recexprlemss1l  7665  recexprlemss1u  7666  uzin  9592  indstr  9625  elfzmlbp  10164
  Copyright terms: Public domain W3C validator