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

Theorem 3bitr4d 311
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 282 . 2 (𝜑 → (𝜓𝜏))
51, 4bitrd 279 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  pr1eqbg  4815  unisucg  6396  fvopab3g  6944  fvimacnvALT  7008  respreima  7017  fmptco  7076  fnnfpeq0  7125  cocan1  7238  cocan2  7239  ordsucelsuc  7758  ordsucsssuc  7759  fnsuppres  8123  smoword  8313  oaword  8497  omword  8518  om00el  8524  oeword  8538  nnaword  8575  nnmword  8581  eldifsucnn  8611  naddss1  8635  naddunif  8638  swoer  8679  erth  8698  brecop  8750  eceqoveq  8762  xpdom2  9012  pw2f1olem  9021  ixpfi2  9295  cantnfrescl  9613  ttrclselem2  9663  rankr1bg  9740  r1pwcl  9784  fseqenlem1  9961  alephord3  10015  alephdom2  10024  engch  10565  fpwwe2lem6  10573  fpwwe2lem8  10575  ltexpi  10839  ltapi  10840  ltmpi  10841  ltsonq  10906  ltmnq  10909  1idpr  10966  addcanpr  10983  axpre-ltadd  11104  axlttri  11227  subsub23  11407  leadd1  11624  ltsub1  11652  ltsub2  11653  leord1  11683  eqord1  11684  lemul1  12008  lediv1  12021  lt2mul2div  12034  lerec  12039  lediv2  12046  le2msq  12056  suprleub  12122  infregelb  12140  ofsubeq0  12151  ofsubge0  12153  avgle1  12394  avgle2  12395  cnref1o  12911  xleneg  13138  xnn0lem1lt  13164  xltadd1  13176  xsubge0  13181  xposdif  13182  xltmul1  13212  supxrleub  13246  infxrgelb  13255  iooneg  13389  iccneg  13390  iccsplit  13403  iccshftr  13404  iccshftl  13406  iccdil  13408  icccntr  13410  fzsplit2  13467  fzaddel  13476  fzrev  13505  predfz  13567  elfzo  13575  nelfzo  13578  fzon  13594  elfzom1b  13672  negmod0  13784  leexp2  14077  ltexp2r  14079  repswsymball  14668  repswsymballbi  14669  cjreb  15009  sqrtlt  15147  limsuplt  15362  o1lo1  15420  rlimresb  15448  lo1eq  15451  rlimeq  15452  o1eq  15453  isercoll  15553  efle  16001  tanaddlem  16049  nndivdvds  16146  moddvds  16148  modmulconst  16171  oddm1even  16226  ltoddhalfle  16244  bitsp1  16312  sadcaddlem  16338  sadadd  16348  sadass  16352  bitsshft  16356  smuval2  16363  smumul  16374  dvdssq  16444  phiprmpw  16649  eulerthlem2  16655  odzdvds  16668  pc2dvds  16752  1arith  16800  imasleval  17424  mreacs  17539  catpropd  17590  oppcsect  17662  funcres2b  17784  fthsect  17813  fthinv  17814  fucsect  17862  fucinv  17863  latnlemlt  18362  latnle  18363  ipole  18424  ipolt  18425  issubg3  18947  eqgid  18983  resghm2b  19027  conjghm  19040  gastacos  19091  resscntz  19113  cntzrec  19115  oppgsubm  19144  oppgsubg  19145  sylow3lem6  19415  lsmcom2  19438  lsmass  19452  ablsubsub23  19604  lsmcomx  19635  subgdmdprd  19814  opprsubrg  20246  lsslss  20425  lbspropd  20563  islbs2  20618  rspsn  20727  prmirred  20898  znfld  20970  lindfmm  21236  lindsmm  21237  lsslindf  21239  lsslinds  21240  islindf4  21247  psrbagconf1o  21341  psrbagconf1oOLD  21342  gsumbagdiaglemOLD  21343  gsumbagdiaglem  21346  mplmonmul  21440  basdif0  22306  neiptopreu  22487  neitr  22534  restlp  22537  cnrest2  22640  cnprest  22643  cnprest2  22644  lmss  22652  lmff  22655  ist1-2  22701  lpcls  22718  perfcls  22719  cmpfi  22762  hauseqlcld  23000  txlm  23002  txkgen  23006  xkopt  23009  idqtop  23060  tgqtop  23066  qtopcn  23068  uffix  23275  fmco  23315  flimrest  23337  lmflf  23359  txflf  23360  fclsrest  23378  cnpfcf  23395  tsmsgsum  23493  tsmsres  23498  tsmsf1o  23499  fmucndlem  23646  ismet2  23689  imasf1oxmet  23731  blres  23787  xmetec  23790  imasf1obl  23847  imasf1oxms  23848  prdsbl  23850  stdbdbl  23876  metrest  23883  metustsym  23914  blval2  23921  metuel2  23924  tngngp  24021  cnbl0  24140  cnblcld  24141  bl2ioo  24158  cncfcnvcn  24291  iihalf2  24299  icoopnst  24305  iocopnst  24306  icopnfcnv  24308  icopnfhmeo  24309  cphorthcom  24568  caucfil  24650  lmclim  24670  cmsss  24718  rrxmet  24775  volsup  24923  dyaddisjlem  24962  mbfeqalem1  25008  mbfeqalem2  25009  mbfeqa  25010  mbfmulc2lem  25014  mbfmax  25016  mbfposr  25019  ismbf3d  25021  mbfimaopnlem  25022  mbfaddlem  25027  mbfsup  25031  mbfinf  25032  0plef  25039  0pledm  25040  i1fmulclem  25070  i1fres  25073  i1fpos  25074  itg1climres  25082  mbfi1fseqlem4  25086  itg2mulclem  25114  itg2monolem1  25118  itg2cnlem1  25129  iblre  25161  iblcn  25166  itgeqa  25181  ellimc2  25244  limcflf  25248  dvreslem  25276  lhop1  25381  ply1remlem  25530  fta1glem2  25534  ofmulrt  25645  plydiveu  25661  plyremlem  25667  quotcan  25672  ulmres  25750  cos11  25892  logleb  25961  argrege0  25969  logdivle  25980  efopn  26016  logccv  26021  cxplt  26052  cxple  26053  cxple2  26055  cxplt2  26056  cxplt3  26058  cxple3  26059  logbleb  26136  logblt  26137  angrtmuld  26161  quad2  26192  atans2  26284  rlimcnp  26318  rlimcnp2  26319  rlimcxp  26326  sqff1o  26534  fsumvma2  26565  dchrptlem2  26616  lgsdilem  26675  lgsne0  26686  lgsqr  26702  lgsquadlem1  26731  lgsquadlem2  26732  m1lgs  26739  2lgslem1a  26742  2lgs  26758  dchrisum0lem1  26867  padicabv  26981  nosupinfsep  27083  oldlim  27219  newbday  27234  sltadd2  27303  sleneg  27347  sltsub2  27366  sltsubsubbd  27371  trgcgrg  27460  colcom  27503  colrot1  27504  ishlg  27547  hlcomb  27548  hlbtwn  27556  lncom  27567  lnrot2  27569  israg  27642  perpcom  27658  hpgcom  27712  colopp  27714  iscgra  27754  isinag  27783  colinearalglem2  27859  axcgrid  27868  uvtx01vtx  28348  iscplgredg  28368  rgrusgrprc  28540  uspgr2wlkeq  28597  clwlkclwwlk  28949  eupth2lem3lem6  29180  fusgr2wsp2nb  29281  nmorepnf  29713  blocnilem  29749  ubthlem1  29815  shscom  30264  pjpreeq  30343  spansncol  30513  cmcm2  30561  hodsi  30720  nmoprepnf  30812  nmfnrepnf  30825  pjssposi  31117  cvcon3  31229  mdsymlem8  31355  dmdsym  31358  disjunsn  31515  fimarab  31562  unipreima  31563  fmptcof2  31576  ressupprn  31608  1stpreima  31623  fpwrelmapffslem  31652  infxrge0gelb  31674  nndiffz1  31692  mgccnv  31862  pwrssmgc  31863  cntzun  31905  isinftm  32020  qusxpid  32154  lindfpropd  32172  lindspropd  32173  lsmssass  32186  nsgmgc  32193  ghmqusker  32201  finexttrb  32354  ist0cld  32417  metidv  32476  metider  32478  pstmxmet  32481  xrge0iifiso  32519  indpi1  32622  prodindf  32625  indf1ofs  32628  aean  32846  brfae  32850  signsply0  33166  signsvfn  33197  reprinrn  33234  subfacp1lem3  33779  subfacp1lem5  33781  fmlafvel  33982  opelco3  34352  sscoid  34501  cgrcomr  34585  ofscom  34595  cgr3permute3  34635  cgr3permute1  34636  cgr3com  34641  colinearperm1  34650  colinearperm3  34651  outsideofcom  34716  opnbnd  34800  filnetlem4  34856  finxpsuclem  35871  wl-equsald  36001  lindsadd  36074  poimirlem23  36104  broucube  36115  heicant  36116  itg2addnclem2  36133  ftc1anclem1  36154  ftc1anclem5  36158  ftc1anclem6  36159  areacirclem5  36173  areacirc  36174  caures  36222  cnpwstotbnd  36259  ismtyima  36265  rrnmet  36291  reheibor  36301  rngosn3  36386  brcosscnvcoss  36899  br1cosscnvxrn  36939  eqvrelth  37076  brpartspart  37238  lcvbr  37486  lkrsc  37562  lshpkrlem1  37575  opltcon3b  37669  cmt2N  37715  cmt3N  37716  cvrcon3b  37742  cvrcmp2  37749  cvlexchb2  37796  cvlatexchb2  37800  2llnmj  38026  4atlem3  38062  4atlem9  38069  4atlem10a  38070  4atlem11a  38073  4atlem12a  38076  4at2  38080  2lplnmj  38088  llnexchb2  38335  lautlt  38557  lautcvr  38558  lautco  38563  ltrnatb  38603  ltrneq2  38614  cdlemefrs29pre00  38861  cdlemefrs29cpre1  38864  cdleme32fva  38903  dibglbN  39632  dochsncom  39848  dochkrsat  39921  lspindp5  40236  mapdh8ab  40243  hdmapip0com  40383  fsuppind  40768  dvdsexpb  40831  sn-ltmul2d  40933  prjsprellsp  40952  lzenom  41096  rmxycomplete  41244  fzneg  41309  modabsdifz  41313  jm2.19  41320  pw2f1ocnv  41364  fzunt  41734  fzuntd  41735  fzunt1d  41736  fzuntgd  41737  sqrtcvallem1  41910  brtrclfv2  42006  rfovcnvf1od  42283  ntrclsfveq1  42339  ntrclsiso  42346  k0004lem2  42427  caofcan  42610  rfcnpre1  43231  rfcnpre2  43243  ellimcabssub0  43865  liminfpnfuz  44064  xlimpnfxnegmnf2  44106  fperdvper  44167  vonvolmbl  44909  readdcnnred  45542  resubcnnred  45543  cndivrenred  45545  requad2  45822  mgmpropd  46076  lco0  46515  lindslininds  46552  ltsubaddb  46602  ltsubsubb  46603  ltsubadd2b  46604  elbigolo1  46650  dig2bits  46707  rrx2pnedifcoorneorr  46810  mofeu  46921  sepnsepo  46963  lubeldm2d  46998  glbeldm2d  46999  thincsect2  47085  thinccic  47088  postcposALT  47108
  Copyright terms: Public domain W3C validator