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

Theorem bitr3d 272
Description: Deduction form of bitr3i 268. (Contributed by NM, 14-May-1993.)
Hypotheses
Ref Expression
bitr3d.1 (𝜑 → (𝜓𝜒))
bitr3d.2 (𝜑 → (𝜓𝜃))
Assertion
Ref Expression
bitr3d (𝜑 → (𝜒𝜃))

Proof of Theorem bitr3d
StepHypRef Expression
1 bitr3d.1 . . 3 (𝜑 → (𝜓𝜒))
21bicomd 214 . 2 (𝜑 → (𝜒𝜓))
3 bitr3d.2 . 2 (𝜑 → (𝜓𝜃))
42, 3bitrd 270 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  3bitr3d  300  3bitr3rd  301  biass  375  19.21t  2240  sbco2  2574  sbco3  2576  sbcom2  2605  sbal1  2620  sbal2  2621  sbal  2622  csbiebt  3746  prsspwg  4542  ssprss  4543  reusv2lem5  5069  copsex2t  5144  copsex2g  5145  ordtri2  5969  onmindif  6026  fnssresb  6212  fcnvres  6295  foelrni  6463  funimass5  6554  fmptco  6617  cbvfo  6766  isocnv  6802  isoini  6810  isoselem  6813  riota2df  6853  ovmpt2dxf  7014  caovcanrd  7065  onmindif2  7240  ordunisuc2  7272  dfom2  7295  ordge1n0  7813  ondif2  7817  oa00  7874  odi  7894  oeoe  7914  eceqoveq  8086  isfinite2  8455  unfilem1  8461  fodomfib  8477  inficl  8568  dffi3  8574  ordiso2  8657  ordtypelem9  8668  cantnfle  8813  cantnf  8835  wemapwe  8839  rankr1a  8944  bnd2  9001  iscard  9082  domtri2  9096  nnsdomel  9097  cardaleph  9193  dfac12lem2  9249  cfss  9370  axcc3  9543  fodomb  9631  iundom2g  9645  inar1  9880  ltpiord  9992  ordpinq  10048  suplem2pr  10158  enreceq  10170  subeq0  10590  negcon1  10616  subexsub  10732  subeqrev  10736  lesub  10790  ltsub13  10792  subge0  10824  mul0or  10950  mulcan1g  10963  div11  10996  divmuleq  11013  ltmuldiv2  11180  lemuldiv2  11187  nn1suc  11324  addltmul  11533  elnnnn0  11600  znn0sub  11688  prime  11722  zbtwnre  12003  xadddi2  12343  supxrbnd  12374  fz1n  12580  fzrev3  12627  fzo0n  12712  fzonlt0  12713  ico01fl0  12842  modsubdir  12961  om2uzlt2i  12972  hashf1lem1  13454  wrdlenge1n0  13549  ccat0  13571  cnpart  14201  sqrt11  14224  sqrtsq2  14230  absdiflt  14278  absdifle  14279  sqreulem  14320  sqreu  14321  eqsqrtor  14327  clim2  14456  climshft2  14534  isercoll  14619  sumrb  14665  supcvg  14808  prodrblem2  14880  sinbnd  15128  cosbnd  15129  sqrt2irr  15197  dvdscmulr  15231  dvdsmulcr  15232  oddm1even  15285  bitsmod  15375  bitsinv1lem  15380  qredeq  15587  cncongr2  15598  isprm3  15612  prmrp  15639  crth  15698  pcdvdsb  15788  pceq0  15790  unbenlem  15827  ramcl  15948  pwselbasb  16351  pwsle  16355  imasleval  16404  xpsfrnel2  16428  acsfn  16522  ismon2  16596  isepi2  16603  epii  16605  fthsect  16787  fthmon  16789  isipodrs  17364  ipodrsfi  17366  gsumval2a  17482  imasmnd2  17530  grpid  17660  grpidrcan  17683  grpidlcan  17684  grplmulf1o  17692  imasgrp2  17733  ghmeqker  17887  ghmf1  17889  gacan  17937  odmulgeq  18173  pgpssslw  18228  efgsfo  18351  efgred  18360  abladdsub4  18418  subgdmdprd  18633  imasring  18819  lspsnss2  19210  0ring01eqbi  19480  gsumbagdiaglem  19582  znf1o  20105  znfld  20114  znunit  20117  znrrg  20119  iporthcom  20188  ip2eq  20206  obsne0  20277  lindfmm  20374  lindsmm  20375  lsslinds  20378  eltg3  20978  eltop  20990  eltop2  20991  eltop3  20992  lmbrf  21276  cncnpi  21294  dfconn2  21434  1stcfb  21460  elptr  21588  xkoccn  21634  txcn  21641  hausdiag  21660  hmeoimaf1o  21785  isfbas  21844  ufileu  21934  alexsubALTlem4  22065  tsmsf1o  22159  ismet2  22349  imasdsf1olem  22389  imasf1oxmet  22391  imasf1omet  22392  xmseq0  22480  imasf1oxms  22505  metucn  22587  nrmmetd  22590  nmgt0  22645  nlmmul0or  22698  xrsxmet  22823  metdseq0  22868  elpi1i  23056  cphsqrtcl2  23196  tchcph  23246  lmmbrf  23270  caucfil  23291  lmclim  23311  cmsss  23357  srabn  23366  ovolfioo  23446  ovolficc  23447  elovolmr  23455  ovolctb  23469  ovolicc2lem3  23498  mbfmulc2lem  23626  mbfimaopnlem  23634  itg2mulclem  23725  iblrelem  23769  ellimc2  23853  mdegle0  24049  fta1glem2  24138  dgreq0  24233  plydivlem4  24263  plydivex  24264  fta1  24275  quotcan  24276  logeftb  24542  quad2  24778  cubic2  24787  dquartlem1  24790  atandm4  24818  fsumharmonic  24950  wilthlem1  25006  basellem8  25026  mumullem2  25118  chpchtsum  25156  logfaclbnd  25159  dchrelbas4  25180  lgsne0  25272  lgsqrlem2  25284  lgsdchrval  25291  lgsquadlem1  25317  lgsquadlem2  25318  2sqlem7  25361  dchrisum0lem1  25417  trgcgrg  25622  tgcgr4  25638  tgcolg  25661  lmiinv  25896  iseqlg  25959  cusgruvtxb  26544  clwwlkn1  27188  eupth2lem3lem3  27401  eupth2lem3lem6  27404  frgr3vlem2  27447  grpoid  27701  nvmeq0  27839  nvgt0  27855  imsmetlem  27871  nmlnogt0  27978  ip2eqi  28038  hvaddcan2  28254  hvmulcan2  28256  hvaddsub4  28261  hi2eq  28288  pjhtheu  28579  lnopeqi  29193  riesz1  29250  jpi  29455  chcv2  29541  cvp  29560  atnemeq0  29562  brabgaf  29743  fmptcof2  29782  funcnvmptOLD  29792  funcnvmpt  29793  nndiffz1  29873  nn0min  29892  xrge0addgt0  30014  smatrcl  30185  lmlim  30316  carsggect  30703  eulerpartlems  30745  eulerpartlemgh  30763  ballotlemfc0  30877  ballotlemfcc  30878  sgnneg  30925  signsvfpn  30985  signsvfnn  30986  reprdifc  31028  bnj1280  31409  elmrsubrn  31738  msubff1  31774  fz0n  31936  slenlt  32196  imageval  32356  nn0prpwlem  32636  filnetlem4  32695  onsuct0  32755  onint1  32763  bj-mdiv  33472  dissneqlem  33502  wl-sbalnae  33657  wl-ax11-lem8  33681  wl-ax11-lem10  33683  sin2h  33710  tan2h  33712  matunitlindflem1  33716  matunitlindflem2  33717  matunitlindf  33718  poimirlem18  33738  poimirlem21  33741  poimirlem24  33744  heicant  33755  mblfinlem3  33759  ovoliunnfl  33762  voliunnfl  33764  volsupnfl  33765  mbfresfi  33766  mbfposadd  33767  itg2addnclem  33771  itg2addnclem2  33772  itg2addnc  33774  itg2gt0cn  33775  itgaddnclem2  33779  ftc1anclem5  33799  areacirclem1  33810  areacirclem4  33813  areacirc  33815  isdmn3  34182  eldmres2  34353  relbrcoss  34507  lcvp  34818  lcv2  34820  lsatnem0  34823  atnem0  35096  cvlsupr2  35121  cvr2N  35189  athgt  35234  2llnmat  35302  pmap11  35540  pmapeq0  35544  2lnat  35562  paddclN  35620  pmapjat1  35631  ltrn2ateq  35959  dihcnvord  37053  dihcnv11  37054  dih0bN  37060  dih0sb  37064  dihlspsnat  37112  dihatexv2  37118  dihglblem6  37119  dochvalr  37136  dochn0nv  37154  djhcvat42  37194  dochsatshp  37230  dochshpsat  37233  dochkrsat2  37235  lcfl5a  37276  lcfl8a  37282  lclkrlem2a  37286  mapdcnvordN  37437  hdmap14lem4a  37650  hgmapeq0  37683  hdmaplkr  37692  hdmapellkr  37693  rmxycomplete  37981  gicabl  38168  ntrneiel  38877  ntrneik4w  38896  ntrneik4  38897  extoimad  38962  radcnvrat  39011  pm14.123b  39124  iotavalb  39128  infxrunb3  40128  climreeq  40323  clim2f  40346  clim2f2  40380  pfxccat3a  42002  dfodd4  42144  oddprmne2  42197  nnsgrpnmnd  42384  ovmpt2rdxf  42683
  Copyright terms: Public domain W3C validator