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

Theorem bitr2d 187
Description: Deduction form of bitr2i 183. (Contributed by NM, 9-Jun-2004.)
Hypotheses
Ref Expression
bitr2d.1 (𝜑 → (𝜓𝜒))
bitr2d.2 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
bitr2d (𝜑 → (𝜃𝜓))

Proof of Theorem bitr2d
StepHypRef Expression
1 bitr2d.1 . . 3 (𝜑 → (𝜓𝜒))
2 bitr2d.2 . . 3 (𝜑 → (𝜒𝜃))
31, 2bitrd 186 . 2 (𝜑 → (𝜓𝜃))
43bicomd 139 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  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3bitrrd  213  3bitr2rd  215  pm5.18dc  815  drex1  1726  elrnmpt1  4674  xpopth  5928  sbcopeq1a  5939  ltnnnq  6961  ltaddsub  7893  leaddsub  7895  posdif  7912  lesub1  7913  ltsub1  7915  lesub0  7936  possumd  8022  ltdivmul  8309  ledivmul  8310  zlem1lt  8776  zltlem1  8777  fzrev2  9466  fz1sbc  9477  elfzp1b  9478  qtri3or  9619  sumsqeq0  9998  sqrtle  10434  sqrtlt  10435  absgt0ap  10497  iser3shft  10699  dvdssubr  10924  gcdn0gt0  11051  divgcdcoprmex  11166
  Copyright terms: Public domain W3C validator