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

Theorem biimpcd 158
 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 154 1 (𝜓 → (𝜑𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  biimpac  296  3impexpbicom  1414  ax16  1785  ax16i  1830  nelneq  2240  nelneq2  2241  nelne1  2398  nelne2  2399  spc2gv  2776  spc3gv  2778  nssne1  3155  nssne2  3156  ifbothdc  3504  difsn  3657  iununir  3896  nbrne1  3947  nbrne2  3948  exmid01  4121  mosubopt  4604  issref  4921  ssimaex  5482  chfnrn  5531  ffnfv  5578  f1elima  5674  dftpos4  6160  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  snon0  6824  exmidonfinlem  7049  enq0sym  7240  prop  7283  prubl  7294  negf1o  8144  0fz1  9825  elfzmlbp  9909  maxleast  10985  negfi  10999  isprm2  11798  nprmdvds1  11820  exmidsbthrlem  13217
 Copyright terms: Public domain W3C validator