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

Theorem 3bitr4d 312
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 283 . 2 (𝜑 → (𝜓𝜏))
51, 4bitrd 280 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  pr1eqbg  4781  fvopab3g  6757  fvimacnvALT  6820  respreima  6829  fmptco  6884  fnnfpeq0  6933  cocan1  7038  cocan2  7039  ordsucelsuc  7525  ordsucsssuc  7526  fnsuppres  7848  smoword  7994  oaword  8165  omword  8186  om00el  8192  oeword  8206  nnaword  8243  nnmword  8249  swoer  8309  erth  8328  brecop  8380  eceqoveq  8392  xpdom2  8601  pw2f1olem  8610  ixpfi2  8811  cantnfrescl  9128  rankr1bg  9221  r1pwcl  9265  fseqenlem1  9439  alephord3  9493  alephdom2  9502  engch  10039  fpwwe2lem7  10047  fpwwe2lem9  10049  ltexpi  10313  ltapi  10314  ltmpi  10315  ltsonq  10380  ltmnq  10383  1idpr  10440  addcanpr  10457  axpre-ltadd  10578  axlttri  10701  subsub23  10880  leadd1  11097  ltsub1  11125  ltsub2  11126  leord1  11156  eqord1  11157  lemul1  11481  lediv1  11494  lt2mul2div  11507  lerec  11512  lediv2  11519  le2msq  11529  suprleub  11596  infregelb  11614  ofsubeq0  11624  ofsubge0  11626  avgle1  11866  avgle2  11867  cnref1o  12374  xleneg  12601  xnn0lem1lt  12627  xltadd1  12639  xsubge0  12644  xposdif  12645  xltmul1  12675  supxrleub  12709  infxrgelb  12718  iooneg  12847  iccneg  12848  iccsplit  12861  iccshftr  12862  iccshftl  12864  iccdil  12866  icccntr  12868  fzsplit2  12922  fzaddel  12931  fzrev  12960  predfz  13022  elfzo  13030  nelfzo  13033  fzon  13048  elfzom1b  13126  negmod0  13236  leexp2  13525  ltexp2r  13527  repswsymball  14131  repswsymballbi  14132  cjreb  14472  sqrtlt  14611  limsuplt  14826  o1lo1  14884  rlimresb  14912  lo1eq  14915  rlimeq  14916  o1eq  14917  isercoll  15014  efle  15461  tanaddlem  15509  nndivdvds  15606  moddvds  15608  modmulconst  15631  oddm1even  15682  ltoddhalfle  15700  bitsp1  15770  sadcaddlem  15796  sadadd  15806  sadass  15810  bitsshft  15814  smuval2  15821  smumul  15832  dvdssq  15901  phiprmpw  16103  eulerthlem2  16109  odzdvds  16122  pc2dvds  16205  1arith  16253  imasleval  16804  mreacs  16919  catpropd  16969  oppcsect  17038  funcres2b  17157  fthsect  17185  fthinv  17186  fucsect  17232  fucinv  17233  latnlemlt  17684  latnle  17685  ipole  17758  ipolt  17759  issubg3  18237  eqgid  18272  resghm2b  18316  conjghm  18329  gastacos  18380  resscntz  18402  cntzrec  18404  oppgsubm  18430  oppgsubg  18431  sylow3lem6  18688  lsmcom2  18711  lsmass  18726  ablsubsub23  18876  lsmcomx  18907  subgdmdprd  19087  opprsubrg  19487  lsslss  19664  lbspropd  19802  islbs2  19857  rspsn  19957  psrbagconf1o  20084  gsumbagdiaglem  20085  mplmonmul  20175  prmirred  20572  znfld  20637  lindfmm  20901  lindsmm  20902  lsslindf  20904  lsslinds  20905  islindf4  20912  basdif0  21491  neiptopreu  21671  neitr  21718  restlp  21721  cnrest2  21824  cnprest  21827  cnprest2  21828  lmss  21836  lmff  21839  ist1-2  21885  lpcls  21902  perfcls  21903  cmpfi  21946  hauseqlcld  22184  txlm  22186  txkgen  22190  xkopt  22193  idqtop  22244  tgqtop  22250  qtopcn  22252  uffix  22459  fmco  22499  flimrest  22521  lmflf  22543  txflf  22544  fclsrest  22562  cnpfcf  22579  tsmsgsum  22676  tsmsres  22681  tsmsf1o  22682  fmucndlem  22829  ismet2  22872  imasf1oxmet  22914  blres  22970  xmetec  22973  imasf1obl  23027  imasf1oxms  23028  prdsbl  23030  stdbdbl  23056  metrest  23063  metustsym  23094  blval2  23101  metuel2  23104  tngngp  23192  cnbl0  23311  cnblcld  23312  bl2ioo  23329  cncfcnvcn  23458  iihalf2  23466  icoopnst  23472  iocopnst  23473  icopnfcnv  23475  icopnfhmeo  23476  cphorthcom  23734  caucfil  23815  lmclim  23835  cmsss  23883  rrxmet  23940  volsup  24086  dyaddisjlem  24125  mbfeqalem1  24171  mbfeqalem2  24172  mbfeqa  24173  mbfmulc2lem  24177  mbfmax  24179  mbfposr  24182  ismbf3d  24184  mbfimaopnlem  24185  mbfaddlem  24190  mbfsup  24194  mbfinf  24195  0plef  24202  0pledm  24203  i1fmulclem  24232  i1fres  24235  i1fpos  24236  itg1climres  24244  mbfi1fseqlem4  24248  itg2mulclem  24276  itg2monolem1  24280  itg2cnlem1  24291  iblre  24323  iblcn  24328  itgeqa  24343  ellimc2  24404  limcflf  24408  dvreslem  24436  lhop1  24540  ply1remlem  24685  fta1glem2  24689  ofmulrt  24800  plydiveu  24816  plyremlem  24822  quotcan  24827  ulmres  24905  cos11  25044  logleb  25113  argrege0  25121  logdivle  25132  efopn  25168  logccv  25173  cxplt  25204  cxple  25205  cxple2  25207  cxplt2  25208  cxplt3  25210  cxple3  25211  logbleb  25288  logblt  25289  angrtmuld  25313  quad2  25344  atans2  25436  rlimcnp  25471  rlimcnp2  25472  rlimcxp  25479  sqff1o  25687  fsumvma2  25718  dchrptlem2  25769  lgsdilem  25828  lgsne0  25839  lgsqr  25855  lgsquadlem1  25884  lgsquadlem2  25885  m1lgs  25892  2lgslem1a  25895  2lgs  25911  dchrisum0lem1  26020  padicabv  26134  trgcgrg  26229  colcom  26272  colrot1  26273  ishlg  26316  hlcomb  26317  hlbtwn  26325  lncom  26336  lnrot2  26338  israg  26411  perpcom  26427  hpgcom  26481  colopp  26483  iscgra  26523  isinag  26552  colinearalglem2  26621  axcgrid  26630  uvtx01vtx  27107  iscplgredg  27127  rgrusgrprc  27299  uspgr2wlkeq  27355  clwlkclwwlk  27708  eupth2lem3lem6  27940  fusgr2wsp2nb  28041  nmorepnf  28473  blocnilem  28509  ubthlem1  28575  shscom  29024  pjpreeq  29103  spansncol  29273  cmcm2  29321  hodsi  29480  nmoprepnf  29572  nmfnrepnf  29585  pjssposi  29877  cvcon3  29989  mdsymlem8  30115  dmdsym  30118  disjunsn  30273  fimarab  30319  unipreima  30320  fmptcof2  30331  1stpreima  30369  fpwrelmapffslem  30395  infxrge0gelb  30417  nndiffz1  30436  cntzun  30623  isinftm  30738  qusxpid  30856  lindfpropd  30870  lindspropd  30871  finexttrb  30952  metidv  31032  metider  31034  pstmxmet  31037  xrge0iifiso  31078  indpi1  31179  prodindf  31182  indf1ofs  31185  aean  31403  brfae  31407  signsply0  31721  signsvfn  31752  reprinrn  31789  subfacp1lem3  32327  subfacp1lem5  32329  fmlafvel  32530  opelco3  32916  sscoid  33272  cgrcomr  33356  ofscom  33366  cgr3permute3  33406  cgr3permute1  33407  cgr3com  33412  colinearperm1  33421  colinearperm3  33422  outsideofcom  33487  opnbnd  33571  filnetlem4  33627  finxpsuclem  34561  wl-equsald  34661  lindsadd  34767  poimirlem23  34797  broucube  34808  heicant  34809  itg2addnclem2  34826  ftc1anclem1  34849  ftc1anclem5  34853  ftc1anclem6  34854  areacirclem5  34868  areacirc  34869  caures  34918  cnpwstotbnd  34958  ismtyima  34964  rrnmet  34990  reheibor  35000  rngosn3  35085  brcosscnvcoss  35561  br1cosscnvxrn  35596  eqvrelth  35728  lcvbr  36039  lkrsc  36115  lshpkrlem1  36128  opltcon3b  36222  cmt2N  36268  cmt3N  36269  cvrcon3b  36295  cvrcmp2  36302  cvlexchb2  36349  cvlatexchb2  36353  2llnmj  36578  4atlem3  36614  4atlem9  36621  4atlem10a  36622  4atlem11a  36625  4atlem12a  36628  4at2  36632  2lplnmj  36640  llnexchb2  36887  lautlt  37109  lautcvr  37110  lautco  37115  ltrnatb  37155  ltrneq2  37166  cdlemefrs29pre00  37413  cdlemefrs29cpre1  37416  cdleme32fva  37455  dibglbN  38184  dochsncom  38400  dochkrsat  38473  lspindp5  38788  mapdh8ab  38795  hdmapip0com  38935  prjsprellsp  39141  lzenom  39247  rmxycomplete  39394  fzneg  39459  modabsdifz  39463  jm2.19  39470  pw2f1ocnv  39514  brtrclfv2  39952  rfovcnvf1od  40230  ntrclsfveq1  40290  ntrclsiso  40297  k0004lem2  40378  caofcan  40535  rfcnpre1  41156  rfcnpre2  41168  ellimcabssub0  41778  liminfpnfuz  41977  xlimpnfxnegmnf2  42019  fperdvper  42083  vonvolmbl  42824  readdcnnred  43384  resubcnnred  43385  cndivrenred  43387  requad2  43635  mgmpropd  43889  lco0  44380  lindslininds  44417  ltsubaddb  44467  ltsubsubb  44468  ltsubadd2b  44469  elbigolo1  44515  dig2bits  44572  rrx2pnedifcoorneorr  44602
  Copyright terms: Public domain W3C validator