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

Theorem bitr4d 256
Description: Deduction form of bitr4i 252. (Contributed by NM, 30-Jun-1993.)
Hypotheses
Ref Expression
bitr4d.1  |-  ( ph  ->  ( ps  <->  ch )
)
bitr4d.2  |-  ( ph  ->  ( th  <->  ch )
)
Assertion
Ref Expression
bitr4d  |-  ( ph  ->  ( ps  <->  th )
)

Proof of Theorem bitr4d
StepHypRef Expression
1 bitr4d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 bitr4d.2 . . 3  |-  ( ph  ->  ( th  <->  ch )
)
32bicomd 201 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 253 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3bitr2d  281  3bitr2rd  282  3bitr4d  285  3bitr4rd  286  bianabs  880  3anibar  1165  sbcom3  2139  sbal1  2190  sbal2  2191  rmob2  3418  disjprg  4433  reuhypd  4664  ordsssuc  4954  opbrop  5069  opelresi  5275  iota1  5555  funbrfv2b  5902  dffn5  5903  dmfco  5932  fneqeql  5980  f1ompt  6038  dff13  6151  fliftcnv  6194  soisores  6208  isotr  6217  isoini  6219  caovord3  6473  releldm2  6835  brtpos  6966  tpostpos  6977  oe1m  7196  oawordri  7201  oalimcl  7211  omlimcl  7229  omabs  7298  iserd  7339  qliftel  7396  qliftfun  7398  qliftf  7401  ecopovsym  7415  pw2f1olem  7623  mapen  7683  suppeqfsuppbi  7845  funsnfsupp  7855  mapfien  7869  supisolem  7934  wemapso2OLD  7980  cantnflem1  8111  cantnflem1OLD  8134  mapfienOLD  8141  wemapwe  8142  wemapweOLD  8143  rankr1clem  8241  rankr1c  8242  ranklim  8265  r1pwOLD  8267  r1pwcl  8268  isfin1-2  8768  isfin1-4  8770  fin71num  8780  axdc3lem2  8834  ltmnq  9353  prlem936  9428  ltsosr  9474  ltasr  9480  xrlenlt  9655  ltxrlt  9658  letri3  9673  ne0gt0  9692  subadd  9828  ltsubadd2  10029  lesubadd2  10031  suble  10036  ltsub23  10038  ltaddpos2  10049  ltsubpos  10050  subge02  10074  ltord2  10088  leord2  10089  ltaddsublt  10182  divmul  10216  divmul3  10218  rec11r  10249  ltdiv1  10412  ltdivmul2  10426  ledivmul2  10428  ltrec  10432  ltdiv2  10436  negiso  10525  infmrgelb  10529  infmrlb  10530  nnle1eq1  10570  avgle1  10784  avgle2  10785  avgle  10786  nn0le0eq0  10830  elz2  10887  znnnlt1  10897  zleltp1  10920  uzin  11122  difrp  11262  xrltlen  11361  dfle2  11362  xrletri3  11367  qbtwnre  11407  xltnegi  11424  supxrre  11528  supxrre1  11531  infmxrre  11536  ixxun  11554  elioo5  11591  elfz5  11689  elfzm11  11758  uzsplit  11759  flbi  11931  flbi2  11932  fznnfl  11968  zmodid2  12003  2submod  12027  lt2sq  12220  le2sq  12221  sqlecan  12253  bcval5  12375  shftfib  12884  mulre  12933  cnpart  13052  sqrlem6  13060  sqrmo  13064  elicc4abs  13131  abs2difabs  13146  cau4  13168  limsupgre  13283  clim2  13306  ello12  13318  ello1mpt2  13324  elo12  13329  lo1resb  13366  o1resb  13368  climeq  13369  climmpt2  13375  isercoll  13469  caucvgb  13481  fsumss  13526  fsumabs  13594  isumshft  13630  geomulcvg  13664  absefib  13810  xpnnenOLD  13820  dvdsval3  13867  dvdseq  13910  ndvdsadd  13943  bitscmp  13965  smupvallem  14010  dvdssq  14075  isprm3  14103  coprmdvds  14120  isprm5  14130  phiprmpw  14183  prmdiv  14192  pc11  14280  pcz  14281  pockthlem  14300  prmreclem2  14312  prmreclem4  14314  prmreclem6  14316  1arith  14322  vdwapun  14369  ramval  14403  rami  14410  ramcl  14424  pwsle  14766  ercpbllem  14822  invsym  15033  funcres2c  15144  latnle  15589  grpinvcnv  15980  subgacs  16110  eqger  16125  gexdvds2  16479  pgpfi1  16489  pgpfi  16499  lsmass  16562  lssnle  16566  lsmdisj3b  16582  lsmhash  16597  ablsubadd  16696  gsumval3OLD  16782  gsumval3lem2  16784  subgdmdprd  16955  pgpfac1lem2  17000  dvdsr02  17179  drngid2  17286  issubrg3  17331  lssacs  17487  lspsnel5  17515  psrbaglefi  17897  psrbaglefiOLD  17898  coe1mul2lem1  18182  prmirred  18398  prmirredOLD  18401  chrdvds  18438  chrcong  18439  chrnzr  18440  znleval  18466  znleval2  18467  cygznlem3  18481  frlmbas  18659  elfilspd  18711  lindfmm  18735  islindf4  18746  islindf5  18747  mdetunilem9  18995  discld  19463  isneip  19479  neiptopnei  19506  lpdifsn  19517  restopnb  19549  restopn2  19551  restdis  19552  restperf  19558  lmbr2  19633  cncls2  19647  cnprest  19663  cnprest2  19664  iscnrm2  19712  ist0-2  19718  cnt0  19720  ist1-3  19723  ishaus2  19725  cmpfi  19781  dfcon2  19793  1stccnp  19836  1stccn  19837  subislly  19855  hausmapdom  19874  kgencn  19930  tx1cn  19983  tx2cn  19984  txcnmpt  19998  txrest  20005  hauseqlcld  20020  tgqtop  20086  qtopcld  20087  qtopcn  20088  ordthmeolem  20175  trfil2  20261  trfil3  20262  trnei  20266  ufildr  20305  fmfg  20323  rnelfm  20327  fmfnfm  20332  elflim  20345  fbflim  20350  flimrest  20357  isflf  20367  cnflf  20376  cnflf2  20377  fclscf  20399  cnfcf  20416  ptcmplem2  20426  ghmcnp  20486  tsmssubm  20517  iscfilu  20664  xmetgt0  20734  prdsxmetlem  20744  elbl2ps  20765  elbl2  20766  blcomps  20769  blcom  20770  xblpnfps  20771  xblpnf  20772  blpnf  20773  xmeter  20809  setsxms  20855  imasf1obl  20864  stdbdbl  20893  metrest  20900  metcn  20919  txmetcn  20924  metuel2  20955  dscopn  20967  xrtgioo  21184  metdstri  21228  cncffvrn  21275  cnmpt2pc  21301  iihalf2  21306  icopnfhmeo  21316  evth2  21333  lmmbr3  21572  iscau3  21590  lmclimf  21615  metcld  21617  cfilucfil3OLD  21630  cfilucfil3  21631  srabn  21673  rrxmet  21708  minveclem4  21720  evthicc2  21745  ovolfioo  21752  ovolficc  21753  ovolgelb  21764  ovoliun  21789  shft2rab  21792  ovolshftlem1  21793  sca2rab  21796  ovolscalem1  21797  ismbl2  21811  ioombl1lem4  21844  mbfmulc2lem  21927  mbfmax  21929  mbfposr  21932  ismbf3d  21934  mbfaddlem  21940  mbfsup  21944  mbfinf  21945  i1f1lem  21969  i1fmulclem  21982  mbfi1fseqlem4  21998  itg2seq  22022  itg2monolem1  22030  itg2cnlem1  22041  itgfsum  22106  ditgneg  22134  limcdif  22153  limcnlp  22155  cnplimc  22164  rolle  22264  mvth  22266  dvne0  22285  lhop1lem  22287  itgsubst  22323  mdegle0  22350  deg1leb  22368  deg1le0  22385  q1peqb  22428  coemulhi  22523  dgrlt  22535  plydivlem3  22563  vieta1lem2  22579  aannenlem1  22596  ulmres  22655  reefiso  22715  pilem3  22720  ellogdm  22892  root1eq1  23001  angpieqvdlem  23031  angpieqvdlem2  23032  quad2  23042  1cubr  23045  quart  23064  rlimcnp  23167  wilthlem2  23215  sgmss  23252  isppw  23260  dvdsflip  23330  dvdsflsumcom  23336  fsumvma  23360  logfac2  23364  chpchtsum  23366  dchrmulcl  23396  dchreq  23405  dchrresb  23406  bclbnd  23427  bposlem1  23431  bposlem5  23435  lgsneg  23466  lgsquadlem1  23501  lgsquadlem2  23502  m1lgs  23509  dchrisumlem3  23548  dchrisum0lem1  23573  trgcgrg  23778  tgellng  23812  lnrot1  23875  islnopp  23985  ismidb  24016  islmib  24025  ttgelitv  24058  axsegconlem6  24097  axeuclidlem  24137  axcontlem2  24140  axcontlem4  24142  axcontlem12  24150  dfconngra1  24543  clwwlkn2  24647  eupath2  24852  frgra3v  24874  drngoi  25281  nmoreltpnf  25556  isblo2  25570  nmlnogt0  25584  phoeqi  25645  ubthlem2  25659  hire  25883  normgt0  25916  ho01i  26619  ho02i  26620  hoeq1  26621  hoeq2  26622  nmopreltpnf  26660  adjeq  26726  leop  26914  leopmul2i  26926  pjnormssi  26959  pjimai  26967  jplem1  27059  mddmd2  27100  mdslmd1lem1  27116  mdslmd1lem2  27117  superpos  27145  atnssm0  27167  dmdbr5ati  27213  disjunsn  27325  fcoinvbr  27333  feqmptdf  27373  ofpreima  27379  funcnv5mpt  27383  isoun  27392  fpwrelmapffslem  27427  fpwrelmap  27428  xgepnf  27442  xlemnf  27443  xrge0infssd  27453  iocinioc2  27462  xrdifh  27463  nndiffz1  27468  xdivmul  27494  isarchi2  27602  fimaproj  27709  sqsscirc2  27764  xrmulc1cn  27785  ismntoplly  27876  esumfsup  27949  1stmbfm  28104  2ndmbfm  28105  mbfmcnt  28112  oms0  28139  eulerpartlems  28172  eulerpartlemd  28178  ballotlemfc0  28304  ballotlemfcc  28305  ballotlemsima  28327  ballotlemfrcn0  28341  sgn3da  28353  erdszelem7  28514  erdszelem9  28516  iscvm  28577  cvmlift3lem4  28640  fprodss  29055  predfz  29258  sltval2  29391  fscgr  29705  seglelin  29741  btwnoutside  29750  lineunray  29772  nndivsub  29897  wl-sbhbt  29977  wl-sbcom2d  29986  wl-sbalnae  29987  wl-ax11-lem8  30007  sin2h  30020  cos2h  30021  ptrest  30023  mblfinlem3  30028  mblfinlem4  30029  ismblfin  30030  itg2addnclem  30041  itg2addnclem2  30042  itg2gt0cn  30045  iblabsnclem  30053  ftc1anclem6  30070  areacirclem2  30083  areacirclem5  30086  areacirc  30087  cldbnd  30119  isfne4  30133  fneval  30145  filnetlem4  30174  cover2  30179  mettrifi  30225  prter3  30598  fz1eqin  30677  diophin  30681  dvdsabsmod0  30903  divalgmodcl  30904  jm2.19  30910  rmxdiophlem  30932  pw2f1ocnv  30954  wepwsolem  30962  gicabl  31022  sdrgacs  31126  idomodle  31129  isdomn3  31140  radcnvrat  31171  lcmdvds  31190  unima  31391  clim2f  31550  2reu4a  32032  dfdfat2  32054  funbrafv2b  32082  dfafn5a  32083  leaddsuble  32157  isfusgracl  32264  lindslinindimp2lem4  32797  snlindsntor  32807  bnj1173  33791  islshpat  34482  lsatnle  34509  ellkr2  34556  lshpkr  34582  lkr0f2  34626  lduallkr3  34627  lkreqN  34635  cvrval2  34739  isat3  34772  glbconN  34841  hlrelat5N  34865  cvrval4N  34878  atlt  34901  1cvrco  34936  pmaple  35225  isline2  35238  isline4N  35241  elpaddn0  35264  elpadd2at2  35271  cdlemkid4  36400  dia0  36519  cdlemm10N  36585  dibglbN  36633  dihmeetlem4preN  36773  dochkrshp3  36855  dvh4dimlem  36910  lcfl5  36963  mapdpglem3  37142  mapdheq  37195  hdmap1eq  37269  hdmapval2lem  37301  hdmapoc  37401  hlhillcs  37428  extoimad  37650
  Copyright terms: Public domain W3C validator