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

Theorem 3bitr4rd 315
 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 285 . 2 (𝜑 → (𝜏𝜓))
4 3bitr4d.2 . 2 (𝜑 → (𝜃𝜓))
53, 4bitr4d 285 1 (𝜑 → (𝜏𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  snssg  4678  inimasn  5980  isof1oidb  7056  oacan  8159  ecdmn0  8321  wemapwe  9146  r1pw  9260  adderpqlem  10367  mulerpqlem  10368  lterpq  10383  ltanq  10384  genpass  10422  readdcan  10805  lemuldiv  11511  msq11  11532  avglt2  11866  qbtwnre  12582  iooshf  12806  clim2c  14856  lo1o1  14883  climabs0  14936  reef11  15466  absefib  15545  efieq1re  15546  nndivides  15611  oddnn02np1  15691  oddge22np1  15692  evennn02n  15693  evennn2n  15694  halfleoddlt  15705  pc2dvds  16207  pcmpt  16220  subsubc  17117  odmulgid  18676  gexdvds  18704  submcmn2  18955  obslbs  20423  cnntr  21887  cndis  21903  cnindis  21904  cnpdis  21905  lmres  21912  cmpfi  22020  ist0-4  22341  txhmeo  22415  tsmssubm  22755  blin  23035  cncfmet  23521  icopnfcnv  23554  lmmbrf  23873  iscauf  23891  causs  23909  mbfposr  24263  itg2gt0  24371  limcflf  24491  limcres  24496  lhop1  24624  dvdsr1p  24769  fsumvma2  25805  vmasum  25807  chpchtsum  25810  bposlem1  25875  iscgrgd  26314  tgcgr4  26332  lnrot1  26424  eqeelen  26705  nbusgreledg  27150  nb3grprlem2  27178  wspthsnwspthsnon  27709  rusgrnumwwlks  27767  clwwlkwwlksb  27846  clwwlknwwlksnb  27847  dmdmd  30090  nfpconfp  30398  funcnvmpt  30437  1stpreimas  30472  xrdifh  30536  swrdrn3  30662  lsmsnorb  31006  rhmpreimacnlem  31249  ismntop  31389  eulerpartlemgh  31758  signslema  31954  fmlafvel  32757  topdifinfindis  34779  leceifl  35062  lindsadd  35066  lindsenlbs  35068  iblabsnclem  35136  ftc1anclem6  35151  areacirclem5  35165  areacirc  35166  brcoss3  35854  lsatfixedN  36321  cdlemg10c  37951  diaglbN  38367  dih1  38598  dihglbcpreN  38612  mapdcv  38972  ellz1  39723  islssfg  40029  proot1ex  40160  eliooshift  42158  clim2cf  42307  dfatdmfcoafv2  43825  sfprmdvdsmersenne  44136  odd2np1ALTV  44207  rrx2plordisom  45151
 Copyright terms: Public domain W3C validator