MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitr2d Structured version   Visualization version   GIF version

Theorem bitr2d 267
Description: Deduction form of bitr2i 263. (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 266 . 2 (𝜑 → (𝜓𝜃))
43bicomd 211 1 (𝜑 → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195
This theorem is referenced by:  3bitrrd  293  3bitr2rd  295  pm5.18  369  ifptru  1016  sbequ12a  2096  elrnmpt1  5278  fndmdif  6210  weniso  6478  sbcopeq1a  7084  cfss  8943  posdif  10366  lesub1  10367  lesub0  10390  possumd  10497  ltdivmul  10743  ledivmul  10744  zlem1lt  11258  zltlem1  11259  negelrp  11692  ioon0  12024  fzn  12179  fzrev2  12225  fz1sbc  12236  elfzp1b  12237  sumsqeq0  12755  fz1isolem  13050  sqrtle  13791  absgt0  13854  isershft  14184  incexc2  14351  dvdssubr  14807  gcdn0gt0  15019  divgcdcoprmex  15160  pcfac  15383  ramval  15492  ltbwe  19235  iunocv  19782  lmbrf  20812  perfcls  20917  ovolscalem1  23001  itg2mulclem  23232  sineq0  23990  efif1olem4  24008  atanord  24367  rlimcnp2  24406  bposlem7  24728  lgsprme0  24777  rpvmasum2  24914  trgcgrg  25124  legov3  25207  opphllem6  25358  ebtwntg  25576  wwlkm1edg  26025  usg2spthonot0  26178  hial2eq2  27150  adjsym  27878  cnvadj  27937  eigvalcl  28006  mddmd  28346  mdslmd2i  28375  elat2  28385  xdivpnfrp  28774  isorng  28932  unitdivcld  29077  indpreima  29216  iooscon  30285  pdivsq  30690  poimirlem26  32404  areacirclem1  32469  isat3  33411  ishlat3N  33458  cvrval5  33518  llnexchb2  33972  lhpoc2N  34118  lhprelat3N  34143  lautcnvle  34192  lautcvr  34195  ltrncnvatb  34241  cdlemb3  34711  cdlemg17h  34773  dih0vbN  35388  djhcvat42  35521  dvh4dimat  35544  mapdordlem2  35743  diophun  36154  jm2.19lem4  36376  uneqsn  37140  xrralrecnnge  38354  flsqrt5  39848  wwlksm1edg  41076  isrnghm  41680  lincfsuppcl  41994  logge0b  42121  loggt0b  42122  logle1b  42123  loglt1b  42124
  Copyright terms: Public domain W3C validator