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

Theorem bitr2d 269
Description: Deduction form of bitr2i 265. (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 268 . 2 (𝜑 → (𝜓𝜃))
43bicomd 213 1 (𝜑 → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  3bitrrd  295  3bitr2rd  297  pm5.18  371  ifptru  1022  sbequ12a  2110  elrnmpt1  5344  fndmdif  6287  weniso  6569  sbcopeq1a  7180  cfss  9047  posdif  10481  lesub1  10482  lesub0  10505  possumd  10612  ltdivmul  10858  ledivmul  10859  zlem1lt  11389  zltlem1  11390  negelrp  11824  ioon0  12159  fzn  12315  fzrev2  12362  fz1sbc  12373  elfzp1b  12374  sumsqeq0  12898  fz1isolem  13199  sqrtle  13951  absgt0  14014  isershft  14344  incexc2  14514  dvdssubr  14970  gcdn0gt0  15182  divgcdcoprmex  15323  pcfac  15546  ramval  15655  ltbwe  19412  iunocv  19965  lmbrf  21004  perfcls  21109  ovolscalem1  23221  itg2mulclem  23453  sineq0  24211  efif1olem4  24229  atanord  24588  rlimcnp2  24627  bposlem7  24949  lgsprme0  24998  rpvmasum2  25135  trgcgrg  25344  legov3  25427  opphllem6  25578  ebtwntg  25796  wwlksm1edg  26670  hial2eq2  27852  adjsym  28580  cnvadj  28639  eigvalcl  28708  mddmd  29048  mdslmd2i  29077  elat2  29087  xdivpnfrp  29468  isorng  29626  unitdivcld  29771  indpreima  29910  ioosconn  30990  pdivsq  31396  poimirlem26  33106  areacirclem1  33171  isat3  34113  ishlat3N  34160  cvrval5  34220  llnexchb2  34674  lhpoc2N  34820  lhprelat3N  34845  lautcnvle  34894  lautcvr  34897  ltrncnvatb  34943  cdlemb3  35413  cdlemg17h  35475  dih0vbN  36090  djhcvat42  36223  dvh4dimat  36246  mapdordlem2  36445  diophun  36856  jm2.19lem4  37078  uneqsn  37842  xrralrecnnge  39112  limsupre2lem  39392  flsqrt5  40838  isrnghm  41210  lincfsuppcl  41520  logge0b  41647  loggt0b  41648  logle1b  41649  loglt1b  41650
  Copyright terms: Public domain W3C validator