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

Theorem 3bitr3d 310
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 282 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3d.3 . 2 (𝜑 → (𝜒𝜏))
53, 4bitrd 280 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  sbcne12  4361  fnprb  6962  fntpb  6963  eloprabga  7250  ordsucuniel  7528  ordsucun  7529  oeoa  8212  ereldm  8326  boxcutc  8493  mapen  8669  mapfien  8859  wemapwe  9148  sdom2en01  9712  prlem936  10457  subcan  10929  mulcan1g  11281  conjmul  11345  ltrec  11510  rebtwnz  12335  xposdif  12643  divelunit  12868  fseq1m1p1  12970  fzm1  12975  fllt  13164  hashfacen  13800  hashf1  13803  ccat0  13917  lenegsq  14668  dvdsmod  15666  bitsmod  15773  smueqlem  15827  rpexp  16052  eulerthlem2  16107  odzdvds  16120  pcelnn  16194  xpsle  16840  isepi  16998  fthmon  17185  pospropd  17732  grpidpropd  17860  mndpropd  17924  mhmpropd  17950  grppropd  18056  ghmnsgima  18320  mndodcong  18599  odf1  18618  odf1o1  18626  sylow3lem6  18686  lsmcntzr  18735  efgredlema  18795  cmnpropd  18845  dprdf11  19074  ringpropd  19261  dvdsrpropd  19375  abvpropd  19542  lmodprop2d  19625  lsspropd  19718  lmhmpropd  19774  lbspropd  19800  lvecvscan  19812  lvecvscan2  19813  assapropd  20029  chrnzr  20605  zndvds0  20625  ip2eq  20725  phlpropd  20727  qtopcn  22250  tsmsf1o  22680  xmetgt0  22895  txmetcnp  23084  metustsym  23092  nlmmul0or  23219  cnmet  23307  evth  23490  isclmp  23628  minveclem3b  23958  mbfposr  24180  itg2cn  24291  iblcnlem  24316  dvcvx  24544  ulm2  24900  efeq1  25040  dcubic  25351  mcubic  25352  dquart  25358  birthdaylem3  25458  ftalem2  25578  issqf  25640  sqff1o  25686  bposlem7  25793  lgsabs1  25839  gausslemma2dlem1a  25868  lgsquadlem2  25884  addsq2reu  25943  dchrisum0lem1  26019  opphllem6  26465  colhp  26483  lmiinv  26505  lmiopp  26515  wlkeq  27342  eupth2lem3lem3  27936  eupth2lem3lem6  27939  nmounbi  28480  ip2eqi  28560  hvmulcan  28776  hvsubcan2  28779  hi2eq  28809  fh2  29323  riesz4i  29767  cvbr4i  30071  xdivpnfrp  30536  isorng  30799  qusker  30845  ellspds  30860  ballotlemfc0  31649  ballotlemfcc  31650  sgnmulsgn  31706  sgnmulsgp  31707  subfacp1lem5  32328  eqfunresadj  32901  sltrec  33175  topfneec2  33601  neibastop3  33607  unccur  34756  cos2h  34764  tan2h  34765  poimirlem25  34798  poimirlem27  34800  dvasin  34859  caures  34916  ismtyima  34962  isdmn3  35233  dmecd  35443  releldmqscoss  35774  tendospcanN  38039  dochsncom  38398  or3or  40249  neicvgel1  40347  rusbcALT  40648  sbcoreleleqVD  41070  climreeq  41770  coseq0  42021  mgmhmpropd  43929  affinecomb1  44617  eenglngeehlnmlem1  44652  2sphere  44664  line2  44667  itscnhlc0yqe  44674  itscnhlc0xyqsol  44680
  Copyright terms: Public domain W3C validator