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

Theorem 3bitr4d 299
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 270 . 2 (𝜑 → (𝜓𝜏))
51, 4bitrd 267 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  fvopab3g  6187  fvimacnvALT  6244  respreima  6252  fmptco  6303  fnnfpeq0  6349  cocan1  6446  cocan2  6447  ordsucelsuc  6914  ordsucsssuc  6915  fnsuppres  7209  smoword  7350  oaword  7516  omword  7537  om00el  7543  oeword  7557  nnaword  7594  nnmword  7600  swoer  7659  erth  7678  brecop  7727  eceqoveq  7740  xpdom2  7940  pw2f1olem  7949  ixpfi2  8147  wemapso2lem  8340  cantnfrescl  8456  rankr1bg  8549  r1pwcl  8593  fseqenlem1  8730  alephord3  8784  alephdom2  8793  engch  9329  fpwwe2lem7  9337  fpwwe2lem9  9339  ltexpi  9603  ltapi  9604  ltmpi  9605  ltsonq  9670  ltmnq  9673  1idpr  9730  addcanpr  9747  axpre-ltadd  9867  axlttri  9988  subsub23  10165  leadd1  10375  ltsub1  10403  ltsub2  10404  leord1  10434  eqord1  10435  lemul1  10754  lediv1  10767  lt2mul2div  10780  lerec  10785  lediv2  10792  le2msq  10802  suprleub  10866  infregelb  10884  ofsubeq0  10894  ofsubge0  10896  avgle1  11149  avgle2  11150  cnref1o  11703  xleneg  11923  xltadd1  11958  xsubge0  11963  xposdif  11964  xltmul1  11994  supxrleub  12028  infxrgelb  12037  iooneg  12163  iccneg  12164  iccsplit  12176  iccshftr  12177  iccshftl  12179  iccdil  12181  icccntr  12183  fzsplit2  12237  fzaddel  12246  fzrev  12273  predfz  12333  elfzo  12341  nelfzo  12344  fzon  12358  elfzom1b  12433  negmod0  12539  leexp2  12777  ltexp2r  12779  repswsymball  13377  repswsymballbi  13378  cjreb  13711  sqrtlt  13850  limsuplt  14058  o1lo1  14116  rlimresb  14144  lo1eq  14147  rlimeq  14148  o1eq  14149  isercoll  14246  efle  14687  tanaddlem  14735  nndivdvds  14827  moddvds  14829  modmulconst  14851  oddm1even  14905  ltoddhalfle  14923  bitsp1  14991  sadcaddlem  15017  sadadd  15027  sadass  15031  bitsshft  15035  smuval2  15042  smumul  15053  dvdssq  15118  phiprmpw  15319  eulerthlem2  15325  odzdvds  15338  pc2dvds  15421  1arith  15469  imasleval  16024  mreacs  16142  catpropd  16192  oppcsect  16261  funcres2b  16380  fthsect  16408  fthinv  16409  fucsect  16455  fucinv  16456  latnlemlt  16907  latnle  16908  ipole  16981  ipolt  16982  issubg3  17435  eqgid  17469  resghm2b  17501  conjghm  17514  gastacos  17566  resscntz  17587  cntzrec  17589  oppgsubm  17615  oppgsubg  17616  sylow3lem6  17870  lsmcom2  17893  lsmass  17906  ablsubsub23  18053  lsmcomx  18082  subgdmdprd  18256  opprsubrg  18624  lsslss  18782  lbspropd  18920  islbs2  18975  rspsn  19075  psrbagconf1o  19195  gsumbagdiaglem  19196  mplmonmul  19285  prmirred  19662  znfld  19728  lindfmm  19985  lindsmm  19986  lsslindf  19988  lsslinds  19989  islindf4  19996  basdif0  20568  neiptopreu  20747  neitr  20794  restlp  20797  cnrest2  20900  cnprest  20903  cnprest2  20904  lmss  20912  lmff  20915  ist1-2  20961  lpcls  20978  perfcls  20979  cmpfi  21021  hauseqlcld  21259  txlm  21261  txkgen  21265  xkopt  21268  idqtop  21319  tgqtop  21325  qtopcn  21327  uffix  21535  fmco  21575  flimrest  21597  lmflf  21619  txflf  21620  fclsrest  21638  cnpfcf  21655  tsmsgsum  21752  tsmsres  21757  tsmsf1o  21758  fmucndlem  21905  ismet2  21948  imasf1oxmet  21990  blres  22046  xmetec  22049  imasf1obl  22103  imasf1oxms  22104  prdsbl  22106  stdbdbl  22132  metrest  22139  metustsym  22170  blval2  22177  metuel2  22180  tngngp  22268  cnbl0  22387  cnblcld  22388  bl2ioo  22403  cncfcnvcn  22532  iihalf2  22540  icoopnst  22546  iocopnst  22547  icopnfcnv  22549  icopnfhmeo  22550  cphorthcom  22809  caucfil  22889  lmclim  22909  cmsss  22955  rrxmet  22999  volsup  23131  dyaddisjlem  23169  mbfeqalem  23215  mbfeqa  23216  mbfmulc2lem  23220  mbfmax  23222  mbfposr  23225  ismbf3d  23227  mbfimaopnlem  23228  mbfaddlem  23233  mbfsup  23237  mbfinf  23238  0plef  23245  0pledm  23246  i1fmulclem  23275  i1fres  23278  i1fpos  23279  itg1climres  23287  mbfi1fseqlem4  23291  itg2mulclem  23319  itg2monolem1  23323  itg2cnlem1  23334  iblre  23366  iblcn  23371  itgeqa  23386  ellimc2  23447  limcflf  23451  dvreslem  23479  lhop1  23581  ply1remlem  23726  fta1glem2  23730  ofmulrt  23841  plydiveu  23857  plyremlem  23863  quotcan  23868  ulmres  23946  cos11  24083  logleb  24153  argrege0  24161  logdivle  24172  efopn  24204  logccv  24209  cxplt  24240  cxple  24241  cxple2  24243  cxplt2  24244  cxplt3  24246  cxple3  24247  logbleb  24321  logblt  24322  angrtmuld  24338  quad2  24366  atans2  24458  rlimcnp  24492  rlimcnp2  24493  rlimcxp  24500  sqff1o  24708  fsumvma2  24739  dchrptlem2  24790  lgsdilem  24849  lgsne0  24860  lgsqr  24876  lgsquadlem1  24905  lgsquadlem2  24906  m1lgs  24913  2lgslem1a  24916  2lgs  24932  dchrisum0lem1  25005  padicabv  25119  trgcgrg  25210  colcom  25253  colrot1  25254  ishlg  25297  hlcomb  25298  hlbtwn  25306  lncom  25317  lnrot2  25319  israg  25392  perpcom  25408  hpgcom  25459  colopp  25461  iscgra  25501  isinag  25529  colinearalglem2  25587  axcgrid  25596  uhgraeq12d  25836  usgraeq12d  25891  nbgrasym  25968  cusgrauvtxb  26024  usg2wlkeq  26236  clwlkisclwwlk  26317  eupath2lem3  26506  usg2spot2nb  26592  nmorepnf  27007  blocnilem  27043  ubthlem1  27110  shscom  27562  pjpreeq  27641  spansncol  27811  cmcm2  27859  hodsi  28018  nmoprepnf  28110  nmfnrepnf  28123  pjssposi  28415  cvcon3  28527  mdsymlem8  28653  dmdsym  28656  disjunsn  28789  fimarab  28825  unipreima  28826  fmptcof2  28839  1stpreima  28867  fpwrelmapffslem  28895  infxrge0gelb  28921  nndiffz1  28936  isinftm  29066  metidv  29263  metider  29265  pstmxmet  29268  xrge0iifiso  29309  indpi1  29411  indf1ofs  29415  aean  29634  brfae  29638  signsply0  29954  signsvfn  29985  subfacp1lem3  30418  subfacp1lem5  30420  opelco3  30923  sscoid  31190  cgrcomr  31274  ofscom  31284  cgr3permute3  31324  cgr3permute1  31325  cgr3com  31330  colinearperm1  31339  colinearperm3  31340  outsideofcom  31405  opnbnd  31490  filnetlem4  31546  finxpsuclem  32410  wl-equsald  32504  wl-sbcom3  32551  poimirlem23  32602  broucube  32613  heicant  32614  itg2addnclem2  32632  ftc1anclem1  32655  ftc1anclem5  32659  ftc1anclem6  32660  areacirclem5  32674  areacirc  32675  caures  32726  cnpwstotbnd  32766  ismtyima  32772  rrnmet  32798  reheibor  32808  rngosn3  32893  lcvbr  33326  lkrsc  33402  lshpkrlem1  33415  opltcon3b  33509  cmt2N  33555  cmt3N  33556  cvrcon3b  33582  cvrcmp2  33589  cvlexchb2  33636  cvlatexchb2  33640  2llnmj  33864  4atlem3  33900  4atlem9  33907  4atlem10a  33908  4atlem11a  33911  4atlem12a  33914  4at2  33918  2lplnmj  33926  llnexchb2  34173  lautlt  34395  lautcvr  34396  lautco  34401  ltrnatb  34441  ltrneq2  34452  cdlemefrs29pre00  34701  cdlemefrs29cpre1  34704  cdleme32fva  34743  dibglbN  35473  dochsncom  35689  dochkrsat  35762  lspindp5  36077  mapdh8ab  36084  hdmapip0com  36227  lzenom  36351  rmxycomplete  36500  fzneg  36567  modabsdifz  36571  jm2.19  36578  pw2f1ocnv  36622  brtrclfv2  37038  rfovcnvf1od  37318  ntrclsfveq1  37378  ntrclsiso  37385  k0004lem2  37466  caofcan  37544  rfcnpre1  38201  rfcnpre2  38213  ellimcabssub0  38684  fperdvper  38808  vonvolmbl  39551  pr1eqbg  40313  nbgrsym  40591  uvtxa01vtx0  40623  iscplgredg  40639  rgrusgrprc  40789  uspgr2wlkeq  40854  clwlkclwwlk  41211  eupth2lem3lem6  41401  fusgr2wsp2nb  41498  mgmpropd  41565  lco0  42010  lindslininds  42047  ltsubaddb  42098  ltsubsubb  42099  ltsubadd2b  42100  elbigolo1  42149  dig2bits  42206
  Copyright terms: Public domain W3C validator