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  1368  ax16  1735  ax16i  1780  nelneq  2180  nelneq2  2181  nelne1  2336  nelne2  2337  spc2gv  2689  spc3gv  2691  nssne1  3056  nssne2  3057  ifbothdc  3382  difsn  3525  iununir  3761  nbrne1  3804  nbrne2  3805  mosubopt  4425  issref  4731  ssimaex  5260  chfnrn  5304  ffnfv  5349  f1elima  5438  dftpos4  5906  tfr1onlemsucaccv  5984  tfrcllemsucaccv  5997  snon0  6435  enq0sym  6673  prop  6716  prubl  6727  negf1o  7542  0fz1  9129  elfzmlbp  9209  maxleast  10226  negfi  10237  isprm2  10632  nprmdvds1  10654
 Copyright terms: Public domain W3C validator