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  4019  fnprb  6513  fntpb  6514  eloprabga  6789  ordsucuniel  7066  ordsucun  7067  oeoa  7722  ereldm  7833  boxcutc  7993  mapen  8165  mapfien  8354  wemapwe  8632  sdom2en01  9162  prlem936  9907  subcan  10374  mulcan1g  10718  conjmul  10780  ltrec  10943  rebtwnz  11825  xposdif  12130  divelunit  12352  fseq1m1p1  12453  fzm1  12458  fllt  12647  hashfacen  13276  hashf1  13279  lenegsq  14104  dvdsmod  15097  bitsmod  15205  smueqlem  15259  rpexp  15479  eulerthlem2  15534  odzdvds  15547  pcelnn  15621  xpsle  16288  isepi  16447  fthmon  16634  pospropd  17181  grpidpropd  17308  mndpropd  17363  mhmpropd  17388  grppropd  17484  ghmnsgima  17731  mndodcong  18007  odf1  18025  odf1o1  18033  sylow3lem6  18093  lsmcntzr  18139  efgredlema  18199  cmnpropd  18248  dprdf11  18468  ringpropd  18628  dvdsrpropd  18742  abvpropd  18890  lmodprop2d  18973  lsspropd  19065  lmhmpropd  19121  lbspropd  19147  lvecvscan  19159  lvecvscan2  19160  assapropd  19375  chrnzr  19926  zndvds0  19947  ip2eq  20046  phlpropd  20048  qtopcn  21565  tsmsf1o  21995  xmetgt0  22210  txmetcnp  22399  metustsym  22407  nlmmul0or  22534  cnmet  22622  evth  22805  isclmp  22943  minveclem3b  23245  mbfposr  23464  itg2cn  23575  iblcnlem  23600  dvcvx  23828  ulm2  24184  efeq1  24320  dcubic  24618  mcubic  24619  dquart  24625  birthdaylem3  24725  ftalem2  24845  issqf  24907  sqff1o  24953  bposlem7  25060  lgsabs1  25106  gausslemma2dlem1a  25135  lgsquadlem2  25151  dchrisum0lem1  25250  opphllem6  25689  colhp  25707  lmiinv  25729  lmiopp  25739  eupth2lem3lem3  27208  eupth2lem3lem6  27211  nmounbi  27759  ip2eqi  27840  hvmulcan  28057  hvsubcan2  28060  hi2eq  28090  fh2  28606  riesz4i  29050  cvbr4i  29354  xdivpnfrp  29769  isorng  29927  ballotlemfc0  30682  ballotlemfcc  30683  sgnmulsgn  30739  sgnmulsgp  30740  subfacp1lem5  31292  eqfunresadj  31785  sltrec  32049  topfneec2  32476  neibastop3  32482  unccur  33522  cos2h  33530  tan2h  33531  poimirlem25  33564  poimirlem27  33566  dvasin  33626  caures  33686  ismtyima  33732  isdmn3  34003  dmecd  34215  tendospcanN  36629  dochsncom  36988  or3or  38636  neicvgel1  38734  rusbcALT  38957  sbc3orgOLD  39059  climreeq  40163  coseq0  40393  mgmhmpropd  42110
  Copyright terms: Public domain W3C validator