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  1067  sbequ12a  2249  elrnmpt1  5829  fndmdif  6808  weniso  7099  sbcopeq1a  7739  snmapen  8579  cfss  9676  posdif  11122  lesub1  11123  lesub0  11146  possumd  11254  ltdivmul  11504  ledivmul  11505  zlem1lt  12023  zltlem1  12024  negelrp  12412  ioon0  12754  fzn  12913  fzrev2  12961  fz1sbc  12973  elfzp1b  12974  sumsqeq0  13532  fz1isolem  13809  sqrtle  14610  absgt0  14674  isershft  15010  incexc2  15183  dvdssubr  15645  gcdn0gt0  15856  divgcdcoprmex  16000  pcfac  16225  ramval  16334  ltbwe  20171  mhpinvcl  20256  iunocv  20741  lmbrf  21784  perfcls  21889  ovolscalem1  24029  itg2mulclem  24262  sineq0  25024  efif1olem4  25042  logge0b  25127  loggt0b  25128  logle1b  25129  loglt1b  25130  atanord  25418  rlimcnp2  25458  bposlem7  25780  lgsprme0  25829  rpvmasum2  26002  trgcgrg  26215  legov3  26298  opphllem6  26452  ebtwntg  26682  wwlksm1edg  27573  clwlkclwwlk2  27695  hial2eq2  28798  adjsym  29524  cnvadj  29583  eigvalcl  29652  mddmd  29992  mdslmd2i  30021  elat2  30031  xdivpnfrp  30523  isorng  30786  unitdivcld  31030  indpreima  31170  ioosconn  32378  pdivsq  32865  poimirlem26  34785  areacirclem1  34849  isat3  36310  ishlat3N  36357  cvrval5  36418  llnexchb2  36872  lhpoc2N  37018  lhprelat3N  37043  lautcnvle  37092  lautcvr  37095  ltrncnvatb  37141  cdlemb3  37609  cdlemg17h  37671  dih0vbN  38285  djhcvat42  38418  dvh4dimat  38441  mapdordlem2  38640  reltsub1  39081  reltsubadd2  39082  diophun  39235  jm2.19lem4  39454  uneqsn  40238  xrralrecnnge  41527  limsupre2lem  41870  prprelb  43510  flsqrt5  43589  isrnghm  43995  lincfsuppcl  44300
  Copyright terms: Public domain W3C validator