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

Theorem bitr2d 281
Description: Deduction form of bitr2i 277. (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 280 . 2 (𝜑 → (𝜓𝜃))
43bicomd 224 1 (𝜑 → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  3bitrrd  307  3bitr2rd  309  pm5.18  383  ifptru  1065  sbequ12a  2246  elrnmpt1  5823  fndmdif  6804  weniso  7096  sbcopeq1a  7737  snmapen  8578  cfss  9675  posdif  11121  lesub1  11122  lesub0  11145  possumd  11253  ltdivmul  11503  ledivmul  11504  zlem1lt  12022  zltlem1  12023  negelrp  12410  ioon0  12752  fzn  12911  fzrev2  12959  fz1sbc  12971  elfzp1b  12972  sumsqeq0  13530  fz1isolem  13807  sqrtle  14608  absgt0  14672  isershft  15008  incexc2  15181  dvdssubr  15643  gcdn0gt0  15854  divgcdcoprmex  15998  pcfac  16223  ramval  16332  ltbwe  20181  mhpinvcl  20267  iunocv  20753  lmbrf  21796  perfcls  21901  ovolscalem1  24041  itg2mulclem  24274  sineq0  25036  efif1olem4  25056  logge0b  25141  loggt0b  25142  logle1b  25143  loglt1b  25144  atanord  25432  rlimcnp2  25471  bposlem7  25793  lgsprme0  25842  rpvmasum2  26015  trgcgrg  26228  legov3  26311  opphllem6  26465  ebtwntg  26695  wwlksm1edg  27586  clwlkclwwlk2  27708  hial2eq2  28811  adjsym  29537  cnvadj  29596  eigvalcl  29665  mddmd  30005  mdslmd2i  30034  elat2  30044  xdivpnfrp  30536  isorng  30799  unitdivcld  31043  indpreima  31183  ioosconn  32391  pdivsq  32878  poimirlem26  34799  areacirclem1  34863  isat3  36323  ishlat3N  36370  cvrval5  36431  llnexchb2  36885  lhpoc2N  37031  lhprelat3N  37056  lautcnvle  37105  lautcvr  37108  ltrncnvatb  37154  cdlemb3  37622  cdlemg17h  37684  dih0vbN  38298  djhcvat42  38431  dvh4dimat  38454  mapdordlem2  38653  reltsub1  39094  reltsubadd2  39095  diophun  39248  jm2.19lem4  39467  uneqsn  40251  xrralrecnnge  41538  limsupre2lem  41881  prprelb  43555  flsqrt5  43634  isrnghm  44091  lincfsuppcl  44396
  Copyright terms: Public domain W3C validator