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

Theorem 3bitr4rd 300
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 270 . 2 (𝜑 → (𝜏𝜓))
4 3bitr4d.2 . 2 (𝜑 → (𝜃𝜓))
53, 4bitr4d 270 1 (𝜑 → (𝜏𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  inimasn  5455  isof1oidb  6452  oacan  7493  ecdmn0  7654  wemapwe  8455  r1pw  8569  adderpqlem  9633  mulerpqlem  9634  lterpq  9649  ltanq  9650  genpass  9688  readdcan  10062  lemuldiv  10755  msq11  10776  avglt2  11121  qbtwnre  11866  iooshf  12082  clim2c  14033  lo1o1  14060  climabs0  14113  reef11  14637  absefib  14716  efieq1re  14717  nndivides  14777  oddnn02np1  14859  oddge22np1  14860  evennn02n  14861  evennn2n  14862  halfleoddlt  14873  pc2dvds  15370  pcmpt  15383  subsubc  16285  odmulgid  17743  gexdvds  17771  submcmn2  18016  obslbs  19841  cnntr  20837  cndis  20853  cnindis  20854  cnpdis  20855  lmres  20862  cmpfi  20969  ist0-4  21290  txhmeo  21364  tsmssubm  21704  blin  21984  cncfmet  22467  icopnfcnv  22497  lmmbrf  22813  iscauf  22831  causs  22849  mbfposr  23170  itg2gt0  23278  limcflf  23396  limcres  23401  lhop1  23526  dvdsr1p  23670  fsumvma2  24684  vmasum  24686  chpchtsum  24689  bposlem1  24754  iscgrgd  25154  tgcgr4  25172  lnrot1  25264  eqeelen  25530  nbgraeledg  25753  nb3graprlem2  25775  cusgra3v  25787  cusgrauvtxb  25818  clwlkisclwwlk2  26112  el2spthonot0  26192  rusgranumwlks  26277  dmdmd  28337  funcnvmptOLD  28644  funcnvmpt  28645  1stpreimas  28660  xrdifh  28726  ismntop  29192  eulerpartlemgh  29561  signslema  29759  topdifinfindis  32164  leceifl  32362  lindsenlbs  32368  iblabsnclem  32437  ftc1anclem6  32454  areacirclem5  32468  areacirc  32469  lsatfixedN  33108  cdlemg10c  34739  diaglbN  35156  dih1  35387  dihglbcpreN  35401  mapdcv  35761  ellz1  36142  islssfg  36452  proot1ex  36592  eliooshift  38370  clim2cf  38511  sfprmdvdsmersenne  39853  odd2np1ALTV  39918  nbusgreledg  40567  nb3grprlem2  40601  wspthsnwspthsnon  41114  rusgrnumwwlks  41169  clwlkclwwlk2  41204
  Copyright terms: Public domain W3C validator