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

Theorem bitr4d 247
Description: Deduction form of bitr4i 243. (Contributed by NM, 5-Aug-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 192 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 244 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3bitr2d  272  3bitr2rd  273  3bitr4d  276  3bitr4rd  277  bianabs  850  3anibar  1123  disjprg  4021  ordsssuc  4481  reuhypd  4563  opbrop  4769  opelresiOLD  4968  opelresi  4969  iota1  5235  funbrfv2b  5569  dffn5  5570  dmfco  5595  fneqeql  5635  f1ompt  5684  dff13  5785  fliftcnv  5812  soisores  5826  isotr  5835  isoini  5837  caovord3  6035  releldm2  6172  brtpos  6245  tpostpos  6256  riota1  6325  riota2df  6327  riotasvdOLD  6350  oe1m  6545  oawordri  6550  oalimcl  6560  omlimcl  6578  omabs  6647  iserd  6688  qliftel  6743  qliftfun  6745  qliftf  6748  ecopovsym  6762  pw2f1olem  6968  mapen  7027  supisolem  7223  wemapso2  7269  cantnflem1  7393  mapfien  7401  wemapwe  7402  rankr1clem  7494  rankr1c  7495  ranklim  7518  r1pwOLD  7520  r1pwcl  7521  isfin1-2  8013  isfin1-4  8015  fin71num  8025  axdc3lem2  8079  ltmnq  8598  prlem936  8673  ltsosr  8718  ltasr  8724  xrlenlt  8892  ltxrlt  8895  letri3  8909  ne0gt0  8927  subadd  9056  ltsubadd2  9247  lesubadd2  9249  suble  9254  ltsub23  9256  ltaddpos2  9267  ltsubpos  9268  subge02  9291  ltord2  9304  leord2  9305  divmul  9429  divmul3  9431  rec11r  9461  ltdiv1  9622  ltdivmul2  9633  ledivmul2  9635  ltrec  9639  ltdiv2  9643  negiso  9732  infmrgelb  9736  infmrlb  9737  nnle1eq1  9776  avgle1  9953  avgle2  9954  avgle  9955  nn0le0eq0  9996  elz2  10042  znnnlt1  10052  zleltp1  10070  uzin  10262  difrp  10389  xrltlen  10482  dfle2  10483  xrletri3  10488  qbtwnre  10528  xltnegi  10545  supxrre  10648  supxrre1  10651  infmxrre  10656  ixxun  10674  elioo5  10710  elfz5  10792  elfzm11  10855  uzsplit  10857  flbi  10948  flbi2  10949  fznnfl  10968  lt2sq  11179  le2sq  11180  sqlecan  11211  bcval5  11332  shftfib  11569  mulre  11608  cnpart  11727  sqrlem6  11735  sqrmo  11739  elicc4abs  11805  abs2difabs  11820  cau4  11842  limsupgre  11957  clim2  11980  ello12  11992  ello1mpt2  11998  elo12  12003  lo1resb  12040  o1resb  12042  climeq  12043  climmpt2  12049  isercoll  12143  caucvgb  12154  fsumss  12200  fsumabs  12261  isumshft  12300  geomulcvg  12334  absefib  12480  xpnnenOLD  12490  dvdsval3  12537  dvdseq  12578  ndvdsadd  12609  bitscmp  12631  smupvallem  12676  dvdssq  12741  isprm3  12769  coprmdvds  12783  isprm5  12793  phiprmpw  12846  prmdiv  12855  pc11  12934  pcz  12935  pockthlem  12954  prmreclem2  12966  prmreclem4  12968  prmreclem6  12970  1arith  12976  vdwapun  13023  ramval  13057  rami  13064  ramcl  13078  pwsle  13393  ercpbllem  13452  invsym  13666  funcres2c  13777  latnle  14193  ismgmid  14389  grpinvcnv  14538  subgacs  14654  eqger  14669  gexdvds2  14898  pgpfi1  14908  pgpfi  14918  lsmass  14981  lssnle  14985  lsmdisj3b  15001  lsmhash  15016  ablsubadd  15115  gsumval3  15193  subgdmdprd  15271  pgpfac1lem2  15312  dvdsr02  15440  drngid2  15530  issubrg3  15575  lssacs  15726  lspsnel5  15754  psrbaglefi  16120  coe1mul2lem1  16346  prmirred  16450  chrdvds  16484  chrcong  16485  chrnzr  16486  znleval  16510  znleval2  16511  cygznlem3  16525  discld  16828  isneip  16844  lpdifsn  16877  restopnb  16908  restopn2  16910  restdis  16911  restperf  16916  lmbr2  16991  cncls2  17004  cnprest  17019  cnprest2  17020  iscnrm2  17068  ist0-2  17074  cnt0  17076  ist1-3  17079  ishaus2  17081  cmpfi  17137  dfcon2  17147  1stccnp  17190  1stccn  17191  subislly  17209  hausmapdom  17228  kgencn  17253  tx1cn  17305  tx2cn  17306  txcnmpt  17320  txrest  17327  hauseqlcld  17342  tgqtop  17405  qtopcld  17406  qtopcn  17407  ordthmeolem  17494  trfil2  17584  trfil3  17585  trnei  17589  ufildr  17628  fmfg  17646  rnelfm  17650  fmfnfm  17655  elflim  17668  fbflim  17673  flimrest  17680  isflf  17690  cnflf  17699  cnflf2  17700  fclscf  17722  cnfcf  17739  ptcmplem2  17749  ghmcnp  17799  tsmssubm  17827  xmetgt0  17924  prdsxmetlem  17934  elbl2  17952  blcom  17954  xblpnf  17955  blpnf  17956  xmeter  17981  setsxms  18027  imasf1obl  18036  stdbdbl  18065  metrest  18072  metcn  18091  txmetcn  18096  dscopn  18098  xrtgioo  18314  metdstri  18357  cncffvrn  18404  cnmpt2pc  18428  iihalf2  18433  icopnfhmeo  18443  evth2  18460  lmmbr3  18688  iscau3  18706  lmclimf  18731  metcld  18733  srabn  18779  minveclem4  18798  evthicc2  18822  ovolfioo  18829  ovolficc  18830  ovolgelb  18841  ovoliun  18866  shft2rab  18869  ovolshftlem1  18870  sca2rab  18873  ovolscalem1  18874  ismbl2  18888  ioombl1lem4  18920  mbfmulc2lem  19004  mbfmax  19006  mbfposr  19009  ismbf3d  19011  mbfaddlem  19017  mbfsup  19021  mbfinf  19022  i1f1lem  19046  i1fmulclem  19059  mbfi1fseqlem4  19075  itg2seq  19099  itg2monolem1  19107  itg2cnlem1  19118  itgfsum  19183  ditgneg  19209  limcdif  19228  limcnlp  19230  cnplimc  19239  rolle  19339  mvth  19341  dvne0  19360  lhop1lem  19362  itgsubst  19398  mdegle0  19465  deg1leb  19483  deg1le0  19499  q1peqb  19542  coemulhi  19637  dgrlt  19649  plydivlem3  19677  vieta1lem2  19693  aannenlem1  19710  ulmres  19769  reefiso  19826  pilem3  19831  ellogdm  19988  root1eq1  20097  angpieqvdlem  20127  angpieqvdlem2  20128  quad2  20137  1cubr  20140  quart  20159  rlimcnp  20262  wilthlem2  20309  sgmss  20346  isppw  20354  dvdsflip  20424  dvdsflsumcom  20430  fsumvma  20454  fsumvma2  20455  logfac2  20458  chpchtsum  20460  dchrmulcl  20490  dchreq  20499  dchrresb  20500  bclbnd  20521  bposlem1  20525  bposlem5  20529  lgsneg  20560  lgsquadlem1  20595  lgsquadlem2  20596  m1lgs  20603  dchrisumlem3  20642  dchrisum0lem1  20667  drngoi  21076  nmoreltpnf  21349  isblo2  21363  nmlnogt0  21377  phoeqi  21438  ubthlem2  21452  hire  21675  normgt0  21708  ho01i  22410  ho02i  22411  hoeq1  22412  hoeq2  22413  nmopreltpnf  22451  adjeq  22517  leop  22705  leopmul2i  22717  pjnormssi  22750  pjimai  22758  jplem1  22850  mddmd2  22891  mdslmd1lem1  22907  mdslmd1lem2  22908  superpos  22936  atnssm0  22958  dmdbr5ati  23004  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemsima  23076  ballotlemfrcn0  23090  xdivmul  23110  xgtpnf  23116  feqmptdf  23230  funcnv5mpt  23238  isoun  23244  iocinioc2  23274  xrdifh  23275  sqsscirc2  23295  xrmulc1cn  23305  1stmbfm  23567  2ndmbfm  23568  mbfmcnt  23575  erdszelem7  23730  erdszelem9  23732  iscvm  23792  cvmlift3lem4  23855  eupath2  23906  zmodid2  24012  predfz  24205  sltval2  24312  dffun10  24455  axsegconlem6  24552  axeuclidlem  24592  axcontlem2  24595  axcontlem4  24597  axcontlem12  24605  fscgr  24705  seglelin  24741  btwnoutside  24750  lineunray  24772  nndivsub  24898  itg2addnclem  24933  itg2addnclem2  24934  areacirclem4  24938  areacirclem6  24941  areacirc  24942  iscst4  25188  subaddv  25682  cldbnd  26255  isfne4  26280  fneval  26298  filnetlem4  26341  cover2  26369  mettrifi  26484  prter3  26761  fz1eqin  26859  diophin  26863  dvdsabsmod0  27090  divalgmodcl  27091  jm2.19  27097  rmxdiophlem  27119  pw2f1ocnv  27141  wepwsolem  27149  elfilspd  27266  gicabl  27274  lindfmm  27308  islindf4  27319  islindf5  27320  sdrgacs  27520  idomodle  27523  isdomn3  27534  2reu4a  27978  dfdfat2  28005  funbrafv2b  28032  dfafn5a  28033  frgra3v  28191  sbcoreleleq  28354  bnj1173  29105  islshpat  29280  lsatnle  29307  ellkr2  29354  lshpkr  29380  lkr0f2  29424  lduallkr3  29425  lkreqN  29433  cvrval2  29537  isat3  29570  glbconN  29639  hlrelat5N  29663  cvrval4N  29676  atlt  29699  1cvrco  29734  pmaple  30023  isline2  30036  isline4N  30039  elpaddn0  30062  elpadd2at2  30069  cdlemkid4  31196  dia0  31315  cdlemm10N  31381  dibglbN  31429  dihmeetlem4preN  31569  dochkrshp3  31651  dvh4dimlem  31706  lcfl5  31759  mapdpglem3  31938  mapdheq  31991  hdmap1eq  32065  hdmapval2lem  32097  hdmapoc  32197  hlhillcs  32224
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