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

Theorem 3bitr4rd 312
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr4d.1 (𝜑 → (𝜓𝜒))
3bitr4d.2 (𝜑 → (𝜃𝜓))
3bitr4d.3 (𝜑 → (𝜏𝜒))
Assertion
Ref Expression
3bitr4rd (𝜑 → (𝜏𝜃))

Proof of Theorem 3bitr4rd
StepHypRef Expression
1 3bitr4d.3 . . 3 (𝜑 → (𝜏𝜒))
2 3bitr4d.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2bitr4d 282 . 2 (𝜑 → (𝜏𝜓))
4 3bitr4d.2 . 2 (𝜑 → (𝜃𝜓))
53, 4bitr4d 282 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:  snssgOLD  4746  inimasn  6109  isof1oidb  7270  oacan  8496  ecdmn0  8696  wemapwe  9634  ttrclselem2  9663  r1pw  9782  adderpqlem  10891  mulerpqlem  10892  lterpq  10907  ltanq  10908  genpass  10946  readdcan  11330  lemuldiv  12036  msq11  12057  avglt2  12393  qbtwnre  13119  iooshf  13344  clim2c  15388  lo1o1  15415  climabs0  15468  reef11  16002  absefib  16081  efieq1re  16082  nndivides  16147  oddnn02np1  16231  oddge22np1  16232  evennn02n  16233  evennn2n  16234  halfleoddlt  16245  pc2dvds  16752  pcmpt  16765  subsubc  17740  odmulgid  19337  gexdvds  19367  submcmn2  19618  obslbs  21139  cnntr  22629  cndis  22645  cnindis  22646  cnpdis  22647  lmres  22654  cmpfi  22762  ist0-4  23083  txhmeo  23157  tsmssubm  23497  blin  23777  cncfmet  24275  icopnfcnv  24308  lmmbrf  24629  iscauf  24647  causs  24665  mbfposr  25019  itg2gt0  25128  limcflf  25248  limcres  25253  lhop1  25381  dvdsr1p  25529  fsumvma2  26565  vmasum  26567  chpchtsum  26570  bposlem1  26635  addscan2  27305  iscgrgd  27458  tgcgr4  27476  lnrot1  27568  eqeelen  27856  nbusgreledg  28304  nb3grprlem2  28332  wspthsnwspthsnon  28864  rusgrnumwwlks  28922  clwwlkwwlksb  29001  clwwlknwwlksnb  29002  dmdmd  31245  nfpconfp  31549  funcnvmpt  31586  1stpreimas  31622  xrdifh  31686  swrdrn3  31812  lsmsnorb  32175  ghmqusker  32201  rhmpreimacnlem  32468  ismntop  32610  eulerpartlemgh  32981  signslema  33177  fmlafvel  33982  topdifinfindis  35820  leceifl  36070  lindsadd  36074  lindsenlbs  36076  iblabsnclem  36144  ftc1anclem6  36159  areacirclem5  36173  areacirc  36174  brcoss3  36898  lsatfixedN  37474  cdlemg10c  39105  diaglbN  39521  dih1  39752  dihglbcpreN  39766  mapdcv  40126  dvdsexpnn0  40830  ellz1  41093  islssfg  41400  proot1ex  41531  eliooshift  43751  clim2cf  43898  dfatdmfcoafv2  45493  sfprmdvdsmersenne  45802  odd2np1ALTV  45873  rrx2plordisom  46816  i0oii  46959  io1ii  46960
  Copyright terms: Public domain W3C validator