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  1324  ax16  1691  ax16i  1735  nelneq  2135  nelneq2  2136  nelne1  2289  nelne2  2290  spc2gv  2637  spc3gv  2639  nssne1  2995  nssne2  2996  difsn  3492  iununir  3729  nbrne1  3772  nbrne2  3773  mosubopt  4348  issref  4650  ssimaex  5177  chfnrn  5221  ffnfv  5266  f1elima  5355  dftpos4  5819  enq0sym  6415  prop  6458  prubl  6469  0fz1  8679  elfzmlbp  8760
  Copyright terms: Public domain W3C validator