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

Theorem bitr2d 271
Description: Deduction form of bitr2i 267. (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 270 . 2 (𝜑 → (𝜓𝜃))
43bicomd 214 1 (𝜑 → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  3bitrrd  297  3bitr2rd  299  pm5.18  372  ifptru  1089  sbequ12a  2282  elrnmpt1  5589  fndmdif  6553  weniso  6838  sbcopeq1a  7462  snmapen  8283  cfss  9382  posdif  10816  lesub1  10817  lesub0  10840  possumd  10947  ltdivmul  11193  ledivmul  11194  zlem1lt  11715  zltlem1  11716  negelrp  12098  ioon0  12439  fzn  12600  fzrev2  12647  fz1sbc  12659  elfzp1b  12660  sumsqeq0  13185  fz1isolem  13482  sqrtle  14244  absgt0  14307  isershft  14637  incexc2  14812  dvdssubr  15270  gcdn0gt0  15478  divgcdcoprmex  15618  pcfac  15840  ramval  15949  ltbwe  19701  iunocv  20256  lmbrf  21299  perfcls  21404  ovolscalem1  23517  itg2mulclem  23750  sineq0  24511  efif1olem4  24529  logge0b  24614  loggt0b  24615  logle1b  24616  loglt1b  24617  atanord  24891  rlimcnp2  24930  bposlem7  25252  lgsprme0  25301  rpvmasum2  25438  trgcgrg  25647  legov3  25730  opphllem6  25881  ebtwntg  26099  wwlksm1edg  27031  hial2eq2  28315  adjsym  29043  cnvadj  29102  eigvalcl  29171  mddmd  29511  mdslmd2i  29540  elat2  29550  xdivpnfrp  29989  isorng  30147  unitdivcld  30295  indpreima  30435  ioosconn  31574  pdivsq  31979  poimirlem26  33767  areacirclem1  33831  isat3  35106  ishlat3N  35153  cvrval5  35214  llnexchb2  35668  lhpoc2N  35814  lhprelat3N  35839  lautcnvle  35888  lautcvr  35891  ltrncnvatb  35937  cdlemb3  36405  cdlemg17h  36467  dih0vbN  37081  djhcvat42  37214  dvh4dimat  37237  mapdordlem2  37436  diophun  37857  jm2.19lem4  38078  uneqsn  38839  xrralrecnnge  40110  limsupre2lem  40454  flsqrt5  42102  isrnghm  42478  lincfsuppcl  42788
  Copyright terms: Public domain W3C validator