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

Theorem 3bitr4d 300
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 271 . 2 (𝜑 → (𝜓𝜏))
51, 4bitrd 268 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  pr1eqbg  4421  fvopab3g  6316  fvimacnvALT  6376  respreima  6384  fmptco  6436  fnnfpeq0  6485  cocan1  6586  cocan2  6587  ordsucelsuc  7064  ordsucsssuc  7065  fnsuppres  7367  smoword  7508  oaword  7674  omword  7695  om00el  7701  oeword  7715  nnaword  7752  nnmword  7758  swoer  7817  erth  7834  brecop  7883  eceqoveq  7895  xpdom2  8096  pw2f1olem  8105  ixpfi2  8305  wemapso2lem  8498  cantnfrescl  8611  rankr1bg  8704  r1pwcl  8748  fseqenlem1  8885  alephord3  8939  alephdom2  8948  engch  9488  fpwwe2lem7  9496  fpwwe2lem9  9498  ltexpi  9762  ltapi  9763  ltmpi  9764  ltsonq  9829  ltmnq  9832  1idpr  9889  addcanpr  9906  axpre-ltadd  10026  axlttri  10147  subsub23  10324  leadd1  10534  ltsub1  10562  ltsub2  10563  leord1  10593  eqord1  10594  lemul1  10913  lediv1  10926  lt2mul2div  10939  lerec  10944  lediv2  10951  le2msq  10961  suprleub  11027  infregelb  11045  ofsubeq0  11055  ofsubge0  11057  avgle1  11310  avgle2  11311  cnref1o  11865  xleneg  12087  xltadd1  12124  xsubge0  12129  xposdif  12130  xltmul1  12160  supxrleub  12194  infxrgelb  12203  iooneg  12330  iccneg  12331  iccsplit  12343  iccshftr  12344  iccshftl  12346  iccdil  12348  icccntr  12350  fzsplit2  12404  fzaddel  12413  fzrev  12441  predfz  12503  elfzo  12511  nelfzo  12514  fzon  12528  elfzom1b  12607  negmod0  12717  leexp2  12955  ltexp2r  12957  repswsymball  13572  repswsymballbi  13573  cjreb  13907  sqrtlt  14046  limsuplt  14254  o1lo1  14312  rlimresb  14340  lo1eq  14343  rlimeq  14344  o1eq  14345  isercoll  14442  efle  14892  tanaddlem  14940  nndivdvds  15036  moddvds  15038  modmulconst  15060  oddm1even  15114  ltoddhalfle  15132  bitsp1  15200  sadcaddlem  15226  sadadd  15236  sadass  15240  bitsshft  15244  smuval2  15251  smumul  15262  dvdssq  15327  phiprmpw  15528  eulerthlem2  15534  odzdvds  15547  pc2dvds  15630  1arith  15678  imasleval  16248  mreacs  16366  catpropd  16416  oppcsect  16485  funcres2b  16604  fthsect  16632  fthinv  16633  fucsect  16679  fucinv  16680  latnlemlt  17131  latnle  17132  ipole  17205  ipolt  17206  issubg3  17659  eqgid  17693  resghm2b  17725  conjghm  17738  gastacos  17789  resscntz  17810  cntzrec  17812  oppgsubm  17838  oppgsubg  17839  sylow3lem6  18093  lsmcom2  18116  lsmass  18129  ablsubsub23  18276  lsmcomx  18305  subgdmdprd  18479  opprsubrg  18849  lsslss  19009  lbspropd  19147  islbs2  19202  rspsn  19302  psrbagconf1o  19422  gsumbagdiaglem  19423  mplmonmul  19512  prmirred  19891  znfld  19957  lindfmm  20214  lindsmm  20215  lsslindf  20217  lsslinds  20218  islindf4  20225  basdif0  20805  neiptopreu  20985  neitr  21032  restlp  21035  cnrest2  21138  cnprest  21141  cnprest2  21142  lmss  21150  lmff  21153  ist1-2  21199  lpcls  21216  perfcls  21217  cmpfi  21259  hauseqlcld  21497  txlm  21499  txkgen  21503  xkopt  21506  idqtop  21557  tgqtop  21563  qtopcn  21565  uffix  21772  fmco  21812  flimrest  21834  lmflf  21856  txflf  21857  fclsrest  21875  cnpfcf  21892  tsmsgsum  21989  tsmsres  21994  tsmsf1o  21995  fmucndlem  22142  ismet2  22185  imasf1oxmet  22227  blres  22283  xmetec  22286  imasf1obl  22340  imasf1oxms  22341  prdsbl  22343  stdbdbl  22369  metrest  22376  metustsym  22407  blval2  22414  metuel2  22417  tngngp  22505  cnbl0  22624  cnblcld  22625  bl2ioo  22642  cncfcnvcn  22771  iihalf2  22779  icoopnst  22785  iocopnst  22786  icopnfcnv  22788  icopnfhmeo  22789  cphorthcom  23047  caucfil  23127  lmclim  23147  cmsss  23193  rrxmet  23237  volsup  23370  dyaddisjlem  23409  mbfeqalem  23454  mbfeqa  23455  mbfmulc2lem  23459  mbfmax  23461  mbfposr  23464  ismbf3d  23466  mbfimaopnlem  23467  mbfaddlem  23472  mbfsup  23476  mbfinf  23477  0plef  23484  0pledm  23485  i1fmulclem  23514  i1fres  23517  i1fpos  23518  itg1climres  23526  mbfi1fseqlem4  23530  itg2mulclem  23558  itg2monolem1  23562  itg2cnlem1  23573  iblre  23605  iblcn  23610  itgeqa  23625  ellimc2  23686  limcflf  23690  dvreslem  23718  lhop1  23822  ply1remlem  23967  fta1glem2  23971  ofmulrt  24082  plydiveu  24098  plyremlem  24104  quotcan  24109  ulmres  24187  cos11  24324  logleb  24394  argrege0  24402  logdivle  24413  efopn  24449  logccv  24454  cxplt  24485  cxple  24486  cxple2  24488  cxplt2  24489  cxplt3  24491  cxple3  24492  logbleb  24566  logblt  24567  angrtmuld  24583  quad2  24611  atans2  24703  rlimcnp  24737  rlimcnp2  24738  rlimcxp  24745  sqff1o  24953  fsumvma2  24984  dchrptlem2  25035  lgsdilem  25094  lgsne0  25105  lgsqr  25121  lgsquadlem1  25150  lgsquadlem2  25151  m1lgs  25158  2lgslem1a  25161  2lgs  25177  dchrisum0lem1  25250  padicabv  25364  trgcgrg  25455  colcom  25498  colrot1  25499  ishlg  25542  hlcomb  25543  hlbtwn  25551  lncom  25562  lnrot2  25564  israg  25637  perpcom  25653  hpgcom  25704  colopp  25706  iscgra  25746  isinag  25774  colinearalglem2  25832  axcgrid  25841  nbgrsymOLD  26309  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  iscplgredg  26369  rgrusgrprc  26541  uspgr2wlkeq  26598  clwlkclwwlk  26968  eupth2lem3lem6  27211  fusgr2wsp2nb  27314  nmorepnf  27751  blocnilem  27787  ubthlem1  27854  shscom  28306  pjpreeq  28385  spansncol  28555  cmcm2  28603  hodsi  28762  nmoprepnf  28854  nmfnrepnf  28867  pjssposi  29159  cvcon3  29271  mdsymlem8  29397  dmdsym  29400  disjunsn  29533  fimarab  29573  unipreima  29574  fmptcof2  29585  1stpreima  29612  fpwrelmapffslem  29635  infxrge0gelb  29659  nndiffz1  29676  isinftm  29863  metidv  30063  metider  30065  pstmxmet  30068  xrge0iifiso  30109  indpi1  30210  prodindf  30213  indf1ofs  30216  aean  30435  brfae  30439  signsply0  30756  signsvfn  30787  reprinrn  30824  subfacp1lem3  31290  subfacp1lem5  31292  opelco3  31802  sscoid  32145  cgrcomr  32229  ofscom  32239  cgr3permute3  32279  cgr3permute1  32280  cgr3com  32285  colinearperm1  32294  colinearperm3  32295  outsideofcom  32360  opnbnd  32445  filnetlem4  32501  finxpsuclem  33364  wl-equsald  33455  wl-sbcom3  33502  poimirlem23  33562  broucube  33573  heicant  33574  itg2addnclem2  33592  ftc1anclem1  33615  ftc1anclem5  33619  ftc1anclem6  33620  areacirclem5  33634  areacirc  33635  caures  33686  cnpwstotbnd  33726  ismtyima  33732  rrnmet  33758  reheibor  33768  rngosn3  33853  brcosscnvcoss  34329  br1cosscnvxrn  34364  lcvbr  34626  lkrsc  34702  lshpkrlem1  34715  opltcon3b  34809  cmt2N  34855  cmt3N  34856  cvrcon3b  34882  cvrcmp2  34889  cvlexchb2  34936  cvlatexchb2  34940  2llnmj  35164  4atlem3  35200  4atlem9  35207  4atlem10a  35208  4atlem11a  35211  4atlem12a  35214  4at2  35218  2lplnmj  35226  llnexchb2  35473  lautlt  35695  lautcvr  35696  lautco  35701  ltrnatb  35741  ltrneq2  35752  cdlemefrs29pre00  36000  cdlemefrs29cpre1  36003  cdleme32fva  36042  dibglbN  36772  dochsncom  36988  dochkrsat  37061  lspindp5  37376  mapdh8ab  37383  hdmapip0com  37526  lzenom  37650  rmxycomplete  37799  fzneg  37866  modabsdifz  37870  jm2.19  37877  pw2f1ocnv  37921  brtrclfv2  38336  rfovcnvf1od  38615  ntrclsfveq1  38675  ntrclsiso  38682  k0004lem2  38763  caofcan  38839  rfcnpre1  39492  rfcnpre2  39504  ellimcabssub0  40167  fperdvper  40451  vonvolmbl  41196  mgmpropd  42100  lco0  42541  lindslininds  42578  ltsubaddb  42629  ltsubsubb  42630  ltsubadd2b  42631  elbigolo1  42676  dig2bits  42733
  Copyright terms: Public domain W3C validator