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

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

Proof of Theorem 3bitr3rd
StepHypRef Expression
1 3bitr3d.3 . 2 (𝜑 → (𝜒𝜏))
2 3bitr3d.1 . . 3 (𝜑 → (𝜓𝜒))
3 3bitr3d.2 . . 3 (𝜑 → (𝜓𝜃))
42, 3bitr3d 270 . 2 (𝜑 → (𝜒𝜃))
51, 4bitr3d 270 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:  wdomtr  8635  ltaddsub  10703  leaddsub  10705  eqneg  10946  sqreulem  14306  brcic  16664  nmzsubg  17842  f1omvdconj  18072  dfod2  18187  odf1o2  18194  cyggenod  18492  lvecvscan  19323  znidomb  20124  mdetunilem9  20643  iccpnfcnv  22962  dvcvx  24002  cxple2  24663  wilthlem1  25014  lgslem1  25242  colinearalglem2  26007  axeuclidlem  26062  axcontlem7  26070  fusgrfisstep  26443  hvmulcan  28266  unopf1o  29112  ballotlemrv  30918  subfacp1lem3  31499  subfacp1lem5  31501  wl-sbcom2d  33674  poimirlem26  33764  areacirclem1  33828  areacirc  33833  cdleme50eq  36346  hdmapeq0  37650  hdmap11  37654  rmxdiophlem  38104  nnsum3primesle9  42206  0ringdif  42394
  Copyright terms: Public domain W3C validator