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

Theorem 3bitr3d 296
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)
Hypotheses
Ref Expression
3bitr3d.1 (𝜑 → (𝜓𝜒))
3bitr3d.2 (𝜑 → (𝜓𝜃))
3bitr3d.3 (𝜑 → (𝜒𝜏))
Assertion
Ref Expression
3bitr3d (𝜑 → (𝜃𝜏))

Proof of Theorem 3bitr3d
StepHypRef Expression
1 3bitr3d.2 . . 3 (𝜑 → (𝜓𝜃))
2 3bitr3d.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2bitr3d 268 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3d.3 . 2 (𝜑 → (𝜒𝜏))
53, 4bitrd 266 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  sbcne12  3937  fnprb  6355  fntpb  6356  eloprabga  6623  ordsucuniel  6893  ordsucun  6894  oeoa  7541  ereldm  7654  boxcutc  7814  mapen  7986  mapfien  8173  wemapwe  8454  sdom2en01  8984  prlem936  9725  subcan  10187  mulcan1g  10529  conjmul  10591  ltrec  10754  rebtwnz  11619  xposdif  11921  divelunit  12141  fseq1m1p1  12239  fzm1  12244  fllt  12424  hashfacen  13047  hashf1  13050  lenegsq  13854  dvdsmod  14834  bitsmod  14942  smueqlem  14996  rpexp  15216  eulerthlem2  15271  odzdvds  15284  pcelnn  15358  xpsle  16010  isepi  16169  fthmon  16356  pospropd  16903  grpidpropd  17030  mndpropd  17085  mhmpropd  17110  grppropd  17206  ghmnsgima  17453  mndodcong  17730  odf1  17748  odf1o1  17756  sylow3lem6  17816  lsmcntzr  17862  efgredlema  17922  cmnpropd  17971  dprdf11  18191  ringpropd  18351  dvdsrpropd  18465  abvpropd  18611  lmodprop2d  18694  lsspropd  18784  lmhmpropd  18840  lbspropd  18866  lvecvscan  18878  lvecvscan2  18879  assapropd  19094  chrnzr  19642  zndvds0  19663  ip2eq  19762  phlpropd  19764  qtopcn  21269  tsmsf1o  21700  xmetgt0  21914  txmetcnp  22103  metustsym  22111  nlmmul0or  22230  cnmet  22317  evth  22497  isclmp  22636  minveclem3b  22924  mbfposr  23142  itg2cn  23253  iblcnlem  23278  dvcvx  23504  ulm2  23860  efeq1  23996  dcubic  24290  mcubic  24291  dquart  24297  birthdaylem3  24397  ftalem2  24517  issqf  24579  sqff1o  24625  bposlem7  24732  lgsabs1  24778  gausslemma2dlem1a  24807  lgsquadlem2  24823  dchrisum0lem1  24922  opphllem6  25362  colhp  25380  lmiinv  25402  lmiopp  25412  cusgra2v  25757  eupath2lem3  26272  nmounbi  26821  ip2eqi  26902  hvmulcan  27119  hvsubcan2  27122  hi2eq  27152  fh2  27668  riesz4i  28112  cvbr4i  28416  xdivpnfrp  28778  isorng  28936  ballotlemfc0  29687  ballotlemfcc  29688  sgnmulsgn  29744  sgnmulsgp  29745  subfacp1lem5  30226  topfneec2  31327  neibastop3  31333  unccur  32365  cos2h  32373  tan2h  32374  poimirlem25  32407  poimirlem27  32409  dvasin  32469  caures  32529  ismtyima  32575  isdmn3  32846  tendospcanN  35133  dochsncom  35492  or3or  37142  neicvgel1  37240  rusbcALT  37465  sbc3orgOLD  37566  climreeq  38484  coseq0  38551  eupth2lem3lem3  41400  eupth2lem3lem6  41403  mgmhmpropd  41577
  Copyright terms: Public domain W3C validator