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

Theorem bitr3d 246
Description: Deduction form of bitr3i 242. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr3d.1  |-  ( ph  ->  ( ps  <->  ch )
)
bitr3d.2  |-  ( ph  ->  ( ps  <->  th )
)
Assertion
Ref Expression
bitr3d  |-  ( ph  ->  ( ch  <->  th )
)

Proof of Theorem bitr3d
StepHypRef Expression
1 bitr3d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21bicomd 192 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
3 bitr3d.2 . 2  |-  ( ph  ->  ( ps  <->  th )
)
42, 3bitrd 244 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3bitrrd  271  3bitr3d  274  3bitr3rd  275  biass  348  sbequ12a  1874  sbco2  2039  sbco3  2041  sbcom  2042  sb9i  2047  sbcom2  2066  sbal1  2078  sbal  2079  csbiebt  3130  copsex2t  4269  copsex2g  4270  ordtri2  4443  onmindif  4498  reusv2lem5  4555  onmindif2  4619  ordunisuc2  4651  dfom2  4674  fnssresb  5372  fcnvres  5434  funimass5  5658  fmptco  5707  cbvfo  5815  isocnv  5843  isoini  5851  isoselem  5854  ovmpt2dxf  5989  caovcanrd  6039  riota2df  6341  ordge1n0  6513  ondif2  6517  oa00  6573  odi  6593  oeoe  6613  eceqoveq  6779  omsucdomOLD  7072  isfinite2  7131  unfilem1  7137  fodomfib  7152  inficl  7194  dffi3  7200  ordiso2  7246  ordtypelem9  7257  cantnfle  7388  cantnf  7411  wemapwe  7416  rankr1a  7524  bnd2  7579  iscard  7624  domtri2  7638  nnsdomel  7639  cardaleph  7732  dfac12lem2  7786  cfss  7907  axcc3  8080  fodomb  8167  iundom2g  8178  inar1  8413  ltpiord  8527  ordpinq  8583  suplem2pr  8693  enreceq  8707  subeq0  9089  negcon1  9115  lesub  9269  ltsub13  9271  subge0  9303  mul0or  9424  div11  9466  divmuleq  9481  ltmuldiv2  9643  lemuldiv2  9652  nn1suc  9783  addltmul  9963  elnnnn0  10023  znn0sub  10081  prime  10108  uzindOLD  10122  zbtwnre  10330  xadddi2  10633  supxrbnd  10663  fz1n  10828  fzrev3  10865  modsubdir  11024  om2uzlt2i  11030  hashf1lem1  11409  cnpart  11741  sqr11  11764  sqrsq2  11770  absdiflt  11817  absdifle  11818  sqreulem  11859  sqreu  11860  eqsqror  11866  clim2  11994  climshft2  12072  isercoll  12157  sumrb  12202  supcvg  12330  sinbnd  12476  cosbnd  12477  sqr2irr  12543  dvdscmulr  12573  dvdsmulcr  12574  oddm1even  12604  bitsmod  12643  bitsinv1lem  12648  isprm3  12783  prmrp  12796  qredeq  12801  crt  12862  pcdvdsb  12937  pceq0  12939  unbenlem  12971  ramcl  13092  pwselbasb  13403  pwsle  13407  imasleval  13459  xpsfrnel2  13483  acsfn  13577  ismon2  13653  isepi2  13660  epii  13662  fthsect  13815  fthmon  13817  isipodrs  14280  ipodrsfi  14282  imasmnd2  14425  gsumval2a  14475  grpid  14533  grplmulf1o  14558  imasgrp2  14626  ghmeqker  14725  ghmf1  14727  gacan  14775  odmulgeq  14886  pgpssslw  14941  efgsfo  15064  efgred  15073  abladdsub4  15131  subgdmdprd  15285  imasrng  15418  lspsnss2  15778  gsumbagdiaglem  16137  znf1o  16521  znfld  16530  znunit  16533  znrrg  16535  iporthcom  16555  ip2eq  16573  obsne0  16641  eltg3  16716  eltop  16728  eltop2  16729  eltop3  16730  lmbrf  17006  cncnpi  17023  dfcon2  17161  1stcfb  17187  elptr  17284  xkoccn  17329  txcn  17336  hausdiag  17355  hmeoimaf1o  17477  isfbas  17540  ufileu  17630  alexsubALTlem4  17760  tsmsf1o  17843  ismet2  17914  imasdsf1olem  17953  imasf1oxmet  17955  imasf1omet  17956  xmseq0  18026  imasf1oxms  18051  nrmmetd  18113  nlmmul0or  18210  xrsxmet  18331  metdseq0  18374  elpi1i  18560  cphsqrcl2  18638  tchcph  18683  lmmbrf  18704  caucfil  18725  lmclim  18744  cmsss  18788  srabn  18793  ovolfioo  18843  ovolficc  18844  elovolmr  18851  ovolctb  18865  ovolicc2lem3  18894  mbfmulc2lem  19018  mbfimaopnlem  19026  itg2mulclem  19117  iblrelem  19161  ellimc2  19243  mdegle0  19479  fta1glem2  19568  dgreq0  19662  plydivlem4  19692  plydivex  19693  fta1  19704  quotcan  19705  logeftb  19953  quad2  20151  cubic2  20160  dquartlem1  20163  atandm4  20191  fsumharmonic  20321  wilthlem1  20322  basellem8  20341  mumullem2  20434  chpchtsum  20474  logfaclbnd  20477  dchrelbas4  20498  lgsne0  20588  lgsqrlem2  20597  lgsdchrval  20602  lgsquadlem1  20609  lgsquadlem2  20610  2sqlem7  20625  dchrisum0lem1  20681  grpoid  20906  grpodiveq  20939  nvsubadd  21229  nvmeq0  21238  nvgt0  21257  imsmetlem  21275  nmlnogt0  21391  ip2eqi  21451  hvaddcan2  21666  hvmulcan2  21668  hvaddsub4  21673  hi2eq  21700  pjhtheu  21989  lnopeqi  22604  riesz1  22661  jpi  22866  chcv2  22952  cvp  22971  atnemeq0  22973  ballotlemfc0  23067  ballotlemfcc  23068  prsspwg  23200  xppreima  23226  fmptcof2  23244  funcnvmptOLD  23249  funcnvmpt  23250  xrge0addgt0  23346  lmlim  23386  eupath2lem3  23918  ghomf1olem  24016  mulcan1g  24099  subeqrev  24107  fz0n  24112  prodrblem2  24154  imageval  24540  onsuct0  24952  onint1  24960  ovoliunnfl  25001  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  itg2gt0cn  25006  itgaddnclem2  25010  areacirclem2  25028  areacirclem3  25029  areacirclem5  25032  areacirc  25034  dffprod  25422  mvecrtol  25576  mvecrtol2  25580  cmp2morp  26061  nn0prpwlem  26341  filnetlem4  26433  isdmn3  26802  rmxycomplete  27105  gicabl  27366  lindfmm  27400  lindsmm  27401  lsslinds  27404  pm14.123b  27729  iotavalb  27733  climreeq  27842  frgra3vlem2  28425  trsbc  28603  bnj1280  29366  sbco2wAUX7  29559  sbco3wAUX7  29561  sbcomwAUX7  29562  sbal1NEW7  29587  sbalNEW7  29588  ax7w6AUX7  29622  sbco2OLD7  29706  sbco3OLD7  29708  sbcomOLD7  29709  sb9iOLD7  29712  sbcom2OLD7  29715  lcvp  29852  lcv2  29854  lsatnem0  29857  atnem0  30130  cvlsupr2  30155  cvr2N  30222  athgt  30267  2llnmat  30335  pmap11  30573  pmapeq0  30577  2lnat  30595  paddclN  30653  pmapjat1  30664  ltrn2ateq  30991  dihcnvord  32086  dihcnv11  32087  dih0bN  32093  dih0sb  32097  dihlspsnat  32145  dihatexv2  32151  dihglblem6  32152  dochvalr  32169  dochn0nv  32187  djhcvat42  32227  dochsatshp  32263  dochshpsat  32266  dochkrsat2  32268  lcfl5a  32309  lcfl8a  32315  lclkrlem2a  32319  mapdcnvordN  32470  hdmap14lem4a  32686  hgmapeq0  32719  hdmaplkr  32728  hdmapellkr  32729
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator