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  4862  xpopth  6155  sbcopeq1a  6166  ltnnnq  7385  ltaddsub  8355  leaddsub  8357  posdif  8374  lesub1  8375  ltsub1  8377  lesub0  8398  possumd  8488  subap0  8562  ltdivmul  8792  ledivmul  8793  zlem1lt  9268  zltlem1  9269  negelrp  9644  fzrev2  10041  fz1sbc  10052  elfzp1b  10053  qtri3or  10199  sumsqeq0  10554  sqrtle  11000  sqrtlt  11001  absgt0ap  11063  iser3shft  11309  dvdssubr  11801  gcdn0gt0  11933  divgcdcoprmex  12056  pcfac  12302  lmbrf  13009  logge0b  13605  loggt0b  13606  logle1b  13607  loglt1b  13608  lgsne0  13733  lgsprme0  13737
  Copyright terms: Public domain W3C validator