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  868  drex1  1770  elrnmpt1  4790  xpopth  6074  sbcopeq1a  6085  ltnnnq  7243  ltaddsub  8210  leaddsub  8212  posdif  8229  lesub1  8230  ltsub1  8232  lesub0  8253  possumd  8343  subap0  8417  ltdivmul  8646  ledivmul  8647  zlem1lt  9122  zltlem1  9123  negelrp  9487  fzrev2  9877  fz1sbc  9888  elfzp1b  9889  qtri3or  10032  sumsqeq0  10383  sqrtle  10820  sqrtlt  10821  absgt0ap  10883  iser3shft  11127  dvdssubr  11550  gcdn0gt0  11677  divgcdcoprmex  11794  lmbrf  12398  logge0b  12990  loggt0b  12991  logle1b  12992  loglt1b  12993
 Copyright terms: Public domain W3C validator