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

Theorem bitr2d 188
Description: Deduction form of bitr2i 184. (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 187 . 2 (𝜑 → (𝜓𝜃))
43bicomd 140 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  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3bitrrd  214  3bitr2rd  216  pm5.18dc  853  drex1  1754  elrnmpt1  4760  xpopth  6042  sbcopeq1a  6053  ltnnnq  7199  ltaddsub  8166  leaddsub  8168  posdif  8185  lesub1  8186  ltsub1  8188  lesub0  8209  possumd  8299  subap0  8373  ltdivmul  8602  ledivmul  8603  zlem1lt  9078  zltlem1  9079  negelrp  9443  fzrev2  9833  fz1sbc  9844  elfzp1b  9845  qtri3or  9988  sumsqeq0  10339  sqrtle  10776  sqrtlt  10777  absgt0ap  10839  iser3shft  11083  dvdssubr  11466  gcdn0gt0  11593  divgcdcoprmex  11710  lmbrf  12311
  Copyright terms: Public domain W3C validator