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

Theorem 3bitr4d 285
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)
Hypotheses
Ref Expression
3bitr4d.1
3bitr4d.2
3bitr4d.3
Assertion
Ref Expression
3bitr4d

Proof of Theorem 3bitr4d
StepHypRef Expression
1 3bitr4d.2 . 2
2 3bitr4d.1 . . 3
3 3bitr4d.3 . . 3
42, 3bitr4d 256 . 2
51, 4bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  r19.12snOLD  4096  sbcbr  4505  fvopab3g  5952  fvimacnvALT  6006  respreima  6016  fmptco  6064  fnnfpeq0  6102  fnsuppresOLD  6131  cocan1  6194  cocan2  6195  ordsucelsuc  6657  ordsucsssuc  6658  fnsuppres  6946  smoword  7056  oaword  7217  omword  7238  om00el  7244  oeword  7258  nnaword  7295  nnmword  7301  swoer  7358  erth  7375  brecop  7423  eceqoveq  7435  xpdom2  7632  pw2f1olem  7641  omsucdomOLD  7733  fisucdomOLD  7743  ixpfi2  7838  wemapso2lem  7999  cantnfrescl  8116  rankr1bg  8242  r1pwcl  8286  fseqenlem1  8426  alephord3  8480  alephdom2  8489  engch  9027  fpwwe2lem7  9035  fpwwe2lem9  9037  ltexpi  9301  ltapi  9302  ltmpi  9303  ltsonq  9368  ltmnq  9371  1idpr  9428  addcanpr  9445  axpre-ltadd  9565  axlttri  9677  subsub23  9848  leadd1  10045  ltsub1  10073  ltsub2  10074  leord1  10105  eqord1  10106  lemul1  10419  lediv1  10432  lt2mul2div  10446  lerec  10452  lediv2  10460  le2msq  10470  suprleub  10532  infmrgelb  10548  ofsubeq0  10558  ofsubge0  10560  avgle1  10803  avgle2  10804  cnref1o  11244  xleneg  11446  xltadd1  11477  xsubge0  11482  xposdif  11483  xltmul1  11513  supxrleub  11547  infmxrgelb  11555  iooneg  11669  iccneg  11670  iccsplit  11682  iccshftr  11683  iccshftl  11685  iccdil  11687  icccntr  11689  fzsplit2  11739  fzaddel  11747  fzrev  11771  elfzo  11831  fzon  11847  elfzom1b  11911  negmod0  12004  leexp2  12220  ltexp2r  12222  repswsymball  12751  repswsymballbi  12752  cjreb  12956  sqrtlt  13095  limsuplt  13302  o1lo1  13360  rlimresb  13388  lo1eq  13391  rlimeq  13392  o1eq  13393  isercoll  13490  efle  13853  tanaddlem  13901  nndivdvds  13992  moddvds  13993  oddm1even  14047  bitsp1  14081  sadcaddlem  14107  sadadd  14117  sadass  14121  bitsshft  14125  smuval2  14132  smumul  14143  dvdssq  14198  phiprmpw  14306  eulerthlem2  14312  odzdvds  14322  pc2dvds  14402  1arith  14445  imasleval  14938  mreacs  15055  catpropd  15104  oppcsect  15168  funcres2b  15266  fthsect  15294  fthinv  15295  fucsect  15341  fucinv  15342  latnlemlt  15714  latnle  15715  ipole  15788  ipolt  15789  issubg3  16219  eqgid  16253  resghm2b  16285  conjghm  16297  gastacos  16348  resscntz  16369  cntzrec  16371  oppgsubm  16397  oppgsubg  16398  sylow3lem6  16652  lsmcom2  16675  lsmass  16688  lsmcomx  16862  subgdmdprd  17081  opprsubrg  17450  lsslss  17607  lbspropd  17745  islbs2  17800  rspsn  17902  psrbagconf1o  18026  gsumbagdiaglem  18027  mplmonmul  18126  prmirred  18525  prmirredOLD  18528  znfld  18599  lindfmm  18862  lindsmm  18863  lsslindf  18865  lsslinds  18866  islindf4  18873  basdif0  19454  neiptopreu  19634  neitr  19681  restlp  19684  cnrest2  19787  cnprest  19790  cnprest2  19791  lmss  19799  lmff  19802  ist1-2  19848  lpcls  19865  perfcls  19866  cmpfi  19908  hauseqlcld  20147  txlm  20149  txkgen  20153  xkopt  20156  idqtop  20207  tgqtop  20213  qtopcn  20215  uffix  20422  fmco  20462  flimrest  20484  lmflf  20506  txflf  20507  fclsrest  20525  cnpfcf  20542  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmsf1o  20647  fmucndlem  20794  ismet2  20836  imasf1oxmet  20878  blres  20934  xmetec  20937  imasf1obl  20991  imasf1oxms  20992  prdsbl  20994  stdbdbl  21020  metrest  21027  metustsymOLD  21064  metustsym  21065  blval2  21078  metuel2  21082  tngngp  21168  cnbl0  21281  cnblcld  21282  bl2ioo  21297  cncfcnvcn  21425  iihalf2  21433  icoopnst  21439  iocopnst  21440  icopnfcnv  21442  icopnfhmeo  21443  cphorthcom  21647  caucfil  21722  lmclim  21741  cmsss  21789  rrxmet  21835  volsup  21966  dyaddisjlem  22004  mbfeqalem  22049  mbfeqa  22050  mbfmulc2lem  22054  mbfmax  22056  mbfposr  22059  ismbf3d  22061  mbfimaopnlem  22062  mbfaddlem  22067  mbfsup  22071  mbfinf  22072  0plef  22079  0pledm  22080  i1fmulclem  22109  i1fres  22112  i1fpos  22113  itg1climres  22121  mbfi1fseqlem4  22125  itg2mulclem  22153  itg2monolem1  22157  itg2cnlem1  22168  iblre  22200  iblcn  22205  itgeqa  22220  ellimc2  22281  limcflf  22285  dvreslem  22313  lhop1  22415  ply1remlem  22563  fta1glem2  22567  ofmulrt  22678  plydiveu  22694  plyremlem  22700  quotcan  22705  ulmres  22783  cos11  22920  logleb  22988  argrege0  22996  logdivle  23007  efopn  23039  logccv  23044  cxplt  23075  cxple  23076  cxple2  23078  cxplt2  23079  cxplt3  23081  cxple3  23082  angrtmuld  23140  quad2  23170  atans2  23262  rlimcnp  23295  rlimcnp2  23296  rlimcxp  23303  sqff1o  23456  fsumvma2  23489  dchrptlem2  23540  lgsdilem  23597  lgsne0  23608  lgsqr  23621  lgsquadlem1  23629  lgsquadlem2  23630  m1lgs  23637  dchrisum0lem1  23701  padicabv  23815  trgcgrg  23906  colcom  23945  colrot1  23946  ishlg  23986  hlcomb  23987  hlbtwn  23995  lncom  24002  lnrot2  24004  israg  24074  perpcom  24090  hpgcom  24136  iscgra  24169  colinearalglem2  24210  axcgrid  24219  uhgraeq12d  24307  usgraeq12d  24362  nbgrasym  24439  cusgrauvtxb  24496  usg2wlkeq  24708  clwlkisclwwlk  24789  eupath2lem3  24979  usg2spot2nb  25065  rngosn3  25428  nvsubsub23  25557  nmorepnf  25683  blocnilem  25719  ubthlem1  25786  shscom  26237  pjpreeq  26316  spansncol  26486  cmcm2  26534  hodsi  26694  nmoprepnf  26786  nmfnrepnf  26799  pjssposi  27091  cvcon3  27203  mdsymlem8  27329  dmdsym  27332  disjunsn  27453  fimarab  27483  unipreima  27484  fmptcof2  27502  1stpreima  27524  fpwrelmapffslem  27555  nndiffz1  27596  isinftm  27725  metidv  27871  metider  27873  pstmxmet  27876  xrge0iifiso  27917  logblt  28022  indpi1  28035  indf1ofs  28039  aean  28216  brfae  28220  signsply0  28508  signsvfn  28539  subfacp1lem3  28626  subfacp1lem5  28628  opelco3  29208  predfz  29283  sscoid  29563  cgrcomr  29647  ofscom  29657  cgr3permute3  29697  cgr3permute1  29698  cgr3com  29703  colinearperm1  29712  colinearperm3  29713  outsideofcom  29778  wl-equsald  29992  wl-sbcom3  30035  heicant  30049  itg2addnclem2  30067  ftc1anclem1  30090  ftc1anclem5  30094  ftc1anclem6  30095  areacirclem5  30111  areacirc  30112  opnbnd  30143  filnetlem4  30199  caures  30253  cnpwstotbnd  30293  ismtyima  30299  rrnmet  30325  reheibor  30335  lzenom  30703  rmxycomplete  30853  fzneg  30920  modabsdifz  30927  jm2.19  30935  pw2f1ocnv  30979  caofcan  31228  rfcnpre1  31394  rfcnpre2  31406  ellimcabssub0  31623  fperdvper  31715  pr1eqbg  32297  isfusgracl  32426  isfusgraclALT  32428  fusgraimpclALT2  32431  mgmpropd  32463  lco0  33028  lindslininds  33065  lcvbr  34746  lkrsc  34822  lshpkrlem1  34835  opltcon3b  34929  cmt2N  34975  cmt3N  34976  cvrcon3b  35002  cvrcmp2  35009  cvlexchb2  35056  cvlatexchb2  35060  2llnmj  35284  4atlem3  35320  4atlem9  35327  4atlem10a  35328  4atlem11a  35331  4atlem12a  35334  4at2  35338  2lplnmj  35346  llnexchb2  35593  lautlt  35815  lautcvr  35816  lautco  35821  ltrnatb  35861  ltrneq2  35872  cdlemefrs29pre00  36121  cdlemefrs29cpre1  36124  cdleme32fva  36163  dibglbN  36893  dochsncom  37109  dochkrsat  37182  lspindp5  37497  mapdh8ab  37504  hdmapip0com  37647
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
  Copyright terms: Public domain W3C validator