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  1301  ax16  1668  ax16i  1712  nelneq  2112  nelneq2  2113  nelne1  2265  nelne2  2266  spc2gv  2612  spc3gv  2614  nssne1  2970  nssne2  2971  difsn  3465  iununir  3702  nbrne1  3745  nbrne2  3746  mosubopt  4321  issref  4623  ssimaex  5148  chfnrn  5192  ffnfv  5237  f1elima  5326  dftpos4  5789  enq0sym  6274  prop  6316  prubl  6327  prnmaddl  6331
  Copyright terms: Public domain W3C validator