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

Theorem 3bitr4rd 301
 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 271 . 2 (𝜑 → (𝜏𝜓))
4 3bitr4d.2 . 2 (𝜑 → (𝜃𝜓))
53, 4bitr4d 271 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:  snssg  4347  inimasn  5585  isof1oidb  6614  oacan  7673  ecdmn0  7832  wemapwe  8632  r1pw  8746  adderpqlem  9814  mulerpqlem  9815  lterpq  9830  ltanq  9831  genpass  9869  readdcan  10248  lemuldiv  10941  msq11  10962  avglt2  11309  qbtwnre  12068  iooshf  12290  clim2c  14280  lo1o1  14307  climabs0  14360  reef11  14893  absefib  14972  efieq1re  14973  nndivides  15037  oddnn02np1  15119  oddge22np1  15120  evennn02n  15121  evennn2n  15122  halfleoddlt  15133  pc2dvds  15630  pcmpt  15643  subsubc  16560  odmulgid  18017  gexdvds  18045  submcmn2  18290  obslbs  20122  cnntr  21127  cndis  21143  cnindis  21144  cnpdis  21145  lmres  21152  cmpfi  21259  ist0-4  21580  txhmeo  21654  tsmssubm  21993  blin  22273  cncfmet  22758  icopnfcnv  22788  lmmbrf  23106  iscauf  23124  causs  23142  mbfposr  23464  itg2gt0  23572  limcflf  23690  limcres  23695  lhop1  23822  dvdsr1p  23966  fsumvma2  24984  vmasum  24986  chpchtsum  24989  bposlem1  25054  iscgrgd  25453  tgcgr4  25471  lnrot1  25563  eqeelen  25829  nbusgreledg  26294  nb3grprlem2  26327  wspthsnwspthsnon  26879  wspthsnwspthsnonOLD  26881  rusgrnumwwlks  26941  clwlkclwwlk2  26969  clwwlkwwlksb  27018  clwwlknwwlksnb  27019  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  dmdmd  29287  funcnvmptOLD  29595  funcnvmpt  29596  1stpreimas  29611  xrdifh  29670  ismntop  30198  eulerpartlemgh  30568  signslema  30767  topdifinfindis  33324  leceifl  33528  lindsenlbs  33534  iblabsnclem  33603  ftc1anclem6  33620  areacirclem5  33634  areacirc  33635  brcoss3  34328  lsatfixedN  34614  cdlemg10c  36244  diaglbN  36661  dih1  36892  dihglbcpreN  36906  mapdcv  37266  ellz1  37647  islssfg  37957  proot1ex  38096  eliooshift  40047  clim2cf  40200  sfprmdvdsmersenne  41845  odd2np1ALTV  41910
 Copyright terms: Public domain W3C validator