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

Theorem 3bitr3d 298
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 270 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3d.3 . 2 (𝜑 → (𝜒𝜏))
53, 4bitrd 268 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:  sbcne12  3977  fnprb  6457  fntpb  6458  eloprabga  6732  ordsucuniel  7009  ordsucun  7010  oeoa  7662  ereldm  7775  boxcutc  7936  mapen  8109  mapfien  8298  wemapwe  8579  sdom2en01  9109  prlem936  9854  subcan  10321  mulcan1g  10665  conjmul  10727  ltrec  10890  rebtwnz  11772  xposdif  12077  divelunit  12299  fseq1m1p1  12399  fzm1  12404  fllt  12590  hashfacen  13221  hashf1  13224  lenegsq  14041  dvdsmod  15031  bitsmod  15139  smueqlem  15193  rpexp  15413  eulerthlem2  15468  odzdvds  15481  pcelnn  15555  xpsle  16222  isepi  16381  fthmon  16568  pospropd  17115  grpidpropd  17242  mndpropd  17297  mhmpropd  17322  grppropd  17418  ghmnsgima  17665  mndodcong  17942  odf1  17960  odf1o1  17968  sylow3lem6  18028  lsmcntzr  18074  efgredlema  18134  cmnpropd  18183  dprdf11  18403  ringpropd  18563  dvdsrpropd  18677  abvpropd  18823  lmodprop2d  18906  lsspropd  18998  lmhmpropd  19054  lbspropd  19080  lvecvscan  19092  lvecvscan2  19093  assapropd  19308  chrnzr  19859  zndvds0  19880  ip2eq  19979  phlpropd  19981  qtopcn  21498  tsmsf1o  21929  xmetgt0  22144  txmetcnp  22333  metustsym  22341  nlmmul0or  22468  cnmet  22556  evth  22739  isclmp  22878  minveclem3b  23180  mbfposr  23400  itg2cn  23511  iblcnlem  23536  dvcvx  23764  ulm2  24120  efeq1  24256  dcubic  24554  mcubic  24555  dquart  24561  birthdaylem3  24661  ftalem2  24781  issqf  24843  sqff1o  24889  bposlem7  24996  lgsabs1  25042  gausslemma2dlem1a  25071  lgsquadlem2  25087  dchrisum0lem1  25186  opphllem6  25625  colhp  25643  lmiinv  25665  lmiopp  25675  eupth2lem3lem3  27070  eupth2lem3lem6  27073  nmounbi  27601  ip2eqi  27682  hvmulcan  27899  hvsubcan2  27902  hi2eq  27932  fh2  28448  riesz4i  28892  cvbr4i  29196  xdivpnfrp  29615  isorng  29773  ballotlemfc0  30528  ballotlemfcc  30529  sgnmulsgn  30585  sgnmulsgp  30586  subfacp1lem5  31140  eqfunresadj  31635  sltrec  31898  topfneec2  32326  neibastop3  32332  unccur  33363  cos2h  33371  tan2h  33372  poimirlem25  33405  poimirlem27  33407  dvasin  33467  caures  33527  ismtyima  33573  isdmn3  33844  tendospcanN  36131  dochsncom  36490  or3or  38139  neicvgel1  38237  rusbcALT  38460  sbc3orgOLD  38562  climreeq  39645  coseq0  39838  mgmhmpropd  41550
  Copyright terms: Public domain W3C validator