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

Theorem biimpcd 157
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 153 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biimpac  292  3impexpbicom  1372  ax16  1741  ax16i  1786  nelneq  2188  nelneq2  2189  nelne1  2345  nelne2  2346  spc2gv  2709  spc3gv  2711  nssne1  3082  nssne2  3083  ifbothdc  3423  difsn  3574  iununir  3812  nbrne1  3862  nbrne2  3863  exmid01  4032  mosubopt  4503  issref  4814  ssimaex  5365  chfnrn  5410  ffnfv  5456  f1elima  5552  dftpos4  6028  tfr1onlemsucaccv  6106  tfrcllemsucaccv  6119  snon0  6643  enq0sym  6989  prop  7032  prubl  7043  negf1o  7858  0fz1  9457  elfzmlbp  9539  maxleast  10642  negfi  10655  isprm2  11373  nprmdvds1  11395  exmidsbthrlem  11867
  Copyright terms: Public domain W3C validator