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  4381  fvopab3g  6264  fvimacnvALT  6322  respreima  6330  fmptco  6382  fnnfpeq0  6429  cocan1  6531  cocan2  6532  ordsucelsuc  7007  ordsucsssuc  7008  fnsuppres  7307  smoword  7448  oaword  7614  omword  7635  om00el  7641  oeword  7655  nnaword  7692  nnmword  7698  swoer  7757  erth  7776  brecop  7825  eceqoveq  7838  xpdom2  8040  pw2f1olem  8049  ixpfi2  8249  wemapso2lem  8442  cantnfrescl  8558  rankr1bg  8651  r1pwcl  8695  fseqenlem1  8832  alephord3  8886  alephdom2  8895  engch  9435  fpwwe2lem7  9443  fpwwe2lem9  9445  ltexpi  9709  ltapi  9710  ltmpi  9711  ltsonq  9776  ltmnq  9779  1idpr  9836  addcanpr  9853  axpre-ltadd  9973  axlttri  10094  subsub23  10271  leadd1  10481  ltsub1  10509  ltsub2  10510  leord1  10540  eqord1  10541  lemul1  10860  lediv1  10873  lt2mul2div  10886  lerec  10891  lediv2  10898  le2msq  10908  suprleub  10974  infregelb  10992  ofsubeq0  11002  ofsubge0  11004  avgle1  11257  avgle2  11258  cnref1o  11812  xleneg  12034  xltadd1  12071  xsubge0  12076  xposdif  12077  xltmul1  12107  supxrleub  12141  infxrgelb  12150  iooneg  12277  iccneg  12278  iccsplit  12290  iccshftr  12291  iccshftl  12293  iccdil  12295  icccntr  12297  fzsplit2  12351  fzaddel  12360  fzrev  12388  predfz  12448  elfzo  12456  nelfzo  12459  fzon  12473  elfzom1b  12551  negmod0  12660  leexp2  12898  ltexp2r  12900  repswsymball  13507  repswsymballbi  13508  cjreb  13844  sqrtlt  13983  limsuplt  14191  o1lo1  14249  rlimresb  14277  lo1eq  14280  rlimeq  14281  o1eq  14282  isercoll  14379  efle  14829  tanaddlem  14877  nndivdvds  14970  moddvds  14972  modmulconst  14994  oddm1even  15048  ltoddhalfle  15066  bitsp1  15134  sadcaddlem  15160  sadadd  15170  sadass  15174  bitsshft  15178  smuval2  15185  smumul  15196  dvdssq  15261  phiprmpw  15462  eulerthlem2  15468  odzdvds  15481  pc2dvds  15564  1arith  15612  imasleval  16182  mreacs  16300  catpropd  16350  oppcsect  16419  funcres2b  16538  fthsect  16566  fthinv  16567  fucsect  16613  fucinv  16614  latnlemlt  17065  latnle  17066  ipole  17139  ipolt  17140  issubg3  17593  eqgid  17627  resghm2b  17659  conjghm  17672  gastacos  17724  resscntz  17745  cntzrec  17747  oppgsubm  17773  oppgsubg  17774  sylow3lem6  18028  lsmcom2  18051  lsmass  18064  ablsubsub23  18211  lsmcomx  18240  subgdmdprd  18414  opprsubrg  18782  lsslss  18942  lbspropd  19080  islbs2  19135  rspsn  19235  psrbagconf1o  19355  gsumbagdiaglem  19356  mplmonmul  19445  prmirred  19824  znfld  19890  lindfmm  20147  lindsmm  20148  lsslindf  20150  lsslinds  20151  islindf4  20158  basdif0  20738  neiptopreu  20918  neitr  20965  restlp  20968  cnrest2  21071  cnprest  21074  cnprest2  21075  lmss  21083  lmff  21086  ist1-2  21132  lpcls  21149  perfcls  21150  cmpfi  21192  hauseqlcld  21430  txlm  21432  txkgen  21436  xkopt  21439  idqtop  21490  tgqtop  21496  qtopcn  21498  uffix  21706  fmco  21746  flimrest  21768  lmflf  21790  txflf  21791  fclsrest  21809  cnpfcf  21826  tsmsgsum  21923  tsmsres  21928  tsmsf1o  21929  fmucndlem  22076  ismet2  22119  imasf1oxmet  22161  blres  22217  xmetec  22220  imasf1obl  22274  imasf1oxms  22275  prdsbl  22277  stdbdbl  22303  metrest  22310  metustsym  22341  blval2  22348  metuel2  22351  tngngp  22439  cnbl0  22558  cnblcld  22559  bl2ioo  22576  cncfcnvcn  22705  iihalf2  22713  icoopnst  22719  iocopnst  22720  icopnfcnv  22722  icopnfhmeo  22723  cphorthcom  22982  caucfil  23062  lmclim  23082  cmsss  23128  rrxmet  23172  volsup  23305  dyaddisjlem  23344  mbfeqalem  23390  mbfeqa  23391  mbfmulc2lem  23395  mbfmax  23397  mbfposr  23400  ismbf3d  23402  mbfimaopnlem  23403  mbfaddlem  23408  mbfsup  23412  mbfinf  23413  0plef  23420  0pledm  23421  i1fmulclem  23450  i1fres  23453  i1fpos  23454  itg1climres  23462  mbfi1fseqlem4  23466  itg2mulclem  23494  itg2monolem1  23498  itg2cnlem1  23509  iblre  23541  iblcn  23546  itgeqa  23561  ellimc2  23622  limcflf  23626  dvreslem  23654  lhop1  23758  ply1remlem  23903  fta1glem2  23907  ofmulrt  24018  plydiveu  24034  plyremlem  24040  quotcan  24045  ulmres  24123  cos11  24260  logleb  24330  argrege0  24338  logdivle  24349  efopn  24385  logccv  24390  cxplt  24421  cxple  24422  cxple2  24424  cxplt2  24425  cxplt3  24427  cxple3  24428  logbleb  24502  logblt  24503  angrtmuld  24519  quad2  24547  atans2  24639  rlimcnp  24673  rlimcnp2  24674  rlimcxp  24681  sqff1o  24889  fsumvma2  24920  dchrptlem2  24971  lgsdilem  25030  lgsne0  25041  lgsqr  25057  lgsquadlem1  25086  lgsquadlem2  25087  m1lgs  25094  2lgslem1a  25097  2lgs  25113  dchrisum0lem1  25186  padicabv  25300  trgcgrg  25391  colcom  25434  colrot1  25435  ishlg  25478  hlcomb  25479  hlbtwn  25487  lncom  25498  lnrot2  25500  israg  25573  perpcom  25589  hpgcom  25640  colopp  25642  iscgra  25682  isinag  25710  colinearalglem2  25768  axcgrid  25777  nbgrsym  26246  uvtxa01vtx0  26278  iscplgredg  26294  rgrusgrprc  26466  uspgr2wlkeq  26523  clwlkclwwlk  26884  eupth2lem3lem6  27073  fusgr2wsp2nb  27172  nmorepnf  27593  blocnilem  27629  ubthlem1  27696  shscom  28148  pjpreeq  28227  spansncol  28397  cmcm2  28445  hodsi  28604  nmoprepnf  28696  nmfnrepnf  28709  pjssposi  29001  cvcon3  29113  mdsymlem8  29239  dmdsym  29242  disjunsn  29379  fimarab  29418  unipreima  29419  fmptcof2  29430  1stpreima  29458  fpwrelmapffslem  29481  infxrge0gelb  29505  nndiffz1  29522  isinftm  29709  metidv  29909  metider  29911  pstmxmet  29914  xrge0iifiso  29955  indpi1  30056  prodindf  30059  indf1ofs  30062  aean  30281  brfae  30285  signsply0  30602  signsvfn  30633  reprinrn  30670  subfacp1lem3  31138  subfacp1lem5  31140  opelco3  31652  sscoid  31995  cgrcomr  32079  ofscom  32089  cgr3permute3  32129  cgr3permute1  32130  cgr3com  32135  colinearperm1  32144  colinearperm3  32145  outsideofcom  32210  opnbnd  32295  filnetlem4  32351  finxpsuclem  33205  wl-equsald  33296  wl-sbcom3  33343  poimirlem23  33403  broucube  33414  heicant  33415  itg2addnclem2  33433  ftc1anclem1  33456  ftc1anclem5  33460  ftc1anclem6  33461  areacirclem5  33475  areacirc  33476  caures  33527  cnpwstotbnd  33567  ismtyima  33573  rrnmet  33599  reheibor  33609  rngosn3  33694  lcvbr  34127  lkrsc  34203  lshpkrlem1  34216  opltcon3b  34310  cmt2N  34356  cmt3N  34357  cvrcon3b  34383  cvrcmp2  34390  cvlexchb2  34437  cvlatexchb2  34441  2llnmj  34665  4atlem3  34701  4atlem9  34708  4atlem10a  34709  4atlem11a  34712  4atlem12a  34715  4at2  34719  2lplnmj  34727  llnexchb2  34974  lautlt  35196  lautcvr  35197  lautco  35202  ltrnatb  35242  ltrneq2  35253  cdlemefrs29pre00  35502  cdlemefrs29cpre1  35505  cdleme32fva  35544  dibglbN  36274  dochsncom  36490  dochkrsat  36563  lspindp5  36878  mapdh8ab  36885  hdmapip0com  37028  lzenom  37152  rmxycomplete  37301  fzneg  37368  modabsdifz  37372  jm2.19  37379  pw2f1ocnv  37423  brtrclfv2  37838  rfovcnvf1od  38118  ntrclsfveq1  38178  ntrclsiso  38185  k0004lem2  38266  caofcan  38342  rfcnpre1  38998  rfcnpre2  39010  ellimcabssub0  39649  fperdvper  39896  vonvolmbl  40638  mgmpropd  41540  lco0  41981  lindslininds  42018  ltsubaddb  42069  ltsubsubb  42070  ltsubadd2b  42071  elbigolo1  42116  dig2bits  42173
  Copyright terms: Public domain W3C validator