Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpcd 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  1327  ax16  1694  ax16i  1738  nelneq  2138  nelneq2  2139  nelne1  2295  nelne2  2296  spc2gv  2643  spc3gv  2645  nssne1  3001  nssne2  3002  ifbothdc  3357  difsn  3501  iununir  3738  nbrne1  3781  nbrne2  3782  mosubopt  4405  issref  4707  ssimaex  5234  chfnrn  5278  ffnfv  5323  f1elima  5412  dftpos4  5878  snon0  6356  enq0sym  6530  prop  6573  prubl  6584  0fz1  8909  elfzmlbp  8990
 Copyright terms: Public domain W3C validator