New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  biimprcd GIF version

Theorem biimprcd 216
 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 213 1 (χ → (φψ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  biimparc  473  ax11i  1647  ax11eq  2193  ax11el  2194  eleq1a  2422  ceqsalg  2883  cgsexg  2890  cgsex2g  2891  cgsex4g  2892  ceqsex  2893  spc2egv  2941  spc3egv  2943  csbiebt  3172  dfiin2g  4000  eqpw1uni  4330  sfintfin  4532  tfinnn  4534  sfinltfin  4535  funcnvuni  5161  fun11iun  5305  funsi  5520  fundmen  6043  dmfrec  6316
 Copyright terms: Public domain W3C validator