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

Theorem biimpcd 148
Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
Hypothesis
Ref Expression
biimpcd.1 (φ → (ψχ))
Assertion
Ref Expression
biimpcd (ψ → (φχ))

Proof of Theorem biimpcd
StepHypRef Expression
1 id 19 . 2 (ψψ)
2 biimpcd.1 . 2 (φ → (ψχ))
31, 2syl5ibcom 144 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
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  biimpac  282  3impexpbicom  1306  ax16  1676  ax16i  1720  nelneq  2120  nelneq2  2121  nelne1  2273  nelne2  2274  spc2gv  2620  spc3gv  2622  nssne1  2978  nssne2  2979  difsn  3475  iununir  3712  nbrne1  3755  nbrne2  3756  mosubopt  4332  issref  4634  ssimaex  5159  chfnrn  5203  ffnfv  5248  f1elima  5337  dftpos4  5800  enq0sym  6287  prop  6329  prubl  6340  prnmaddl  6344
  Copyright terms: Public domain W3C validator