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

Theorem bitr2d 182
Description: Deduction form of bitr2i 178. (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 181 . 2 (𝜑 → (𝜓𝜃))
43bicomd 133 1 (𝜑 → (𝜃𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3bitrrd  208  3bitr2rd  210  pm5.18dc  788  drex1  1695  elrnmpt1  4613  xpopth  5830  sbcopeq1a  5841  ltnnnq  6579  ltaddsub  7505  leaddsub  7507  posdif  7524  lesub1  7525  ltsub1  7527  lesub0  7548  possumd  7634  ltdivmul  7917  ledivmul  7918  zlem1lt  8358  zltlem1  8359  fzrev2  9049  fz1sbc  9060  elfzp1b  9061  qtri3or  9200  sumsqeq0  9498  sqrtle  9863  sqrtlt  9864  absgt0ap  9926  dvdssubr  10153
  Copyright terms: Public domain W3C validator