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  878  drex1  1791  elrnmpt1  4860  xpopth  6152  sbcopeq1a  6163  ltnnnq  7372  ltaddsub  8342  leaddsub  8344  posdif  8361  lesub1  8362  ltsub1  8364  lesub0  8385  possumd  8475  subap0  8549  ltdivmul  8779  ledivmul  8780  zlem1lt  9255  zltlem1  9256  negelrp  9631  fzrev2  10028  fz1sbc  10039  elfzp1b  10040  qtri3or  10186  sumsqeq0  10541  sqrtle  10987  sqrtlt  10988  absgt0ap  11050  iser3shft  11296  dvdssubr  11788  gcdn0gt0  11920  divgcdcoprmex  12043  pcfac  12289  lmbrf  12968  logge0b  13564  loggt0b  13565  logle1b  13566  loglt1b  13567  lgsne0  13692  lgsprme0  13696
  Copyright terms: Public domain W3C validator