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

Theorem 3bitr3d 300
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 272 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3d.3 . 2 (𝜑 → (𝜒𝜏))
53, 4bitrd 270 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  sbcne12  4190  fnprb  6700  fntpb  6701  eloprabga  6980  ordsucuniel  7257  ordsucun  7258  oeoa  7917  ereldm  8028  boxcutc  8191  mapen  8366  mapfien  8555  wemapwe  8844  sdom2en01  9412  prlem936  10157  subcan  10624  mulcan1g  10968  conjmul  11030  ltrec  11193  rebtwnz  12009  xposdif  12313  divelunit  12540  fseq1m1p1  12641  fzm1  12646  fllt  12834  hashfacen  13458  hashf1  13461  lenegsq  14286  dvdsmod  15276  bitsmod  15380  smueqlem  15434  rpexp  15652  eulerthlem2  15707  odzdvds  15720  pcelnn  15794  xpsle  16449  isepi  16607  fthmon  16794  pospropd  17342  grpidpropd  17469  mndpropd  17524  mhmpropd  17549  grppropd  17645  ghmnsgima  17889  mndodcong  18165  odf1  18183  odf1o1  18191  sylow3lem6  18251  lsmcntzr  18297  efgredlema  18357  cmnpropd  18406  dprdf11  18627  ringpropd  18787  dvdsrpropd  18901  abvpropd  19049  lmodprop2d  19132  lsspropd  19227  lmhmpropd  19283  lbspropd  19309  lvecvscan  19321  lvecvscan2  19322  assapropd  19539  chrnzr  20089  zndvds0  20109  ip2eq  20211  phlpropd  20213  qtopcn  21735  tsmsf1o  22165  xmetgt0  22380  txmetcnp  22569  metustsym  22577  nlmmul0or  22704  cnmet  22792  evth  22975  isclmp  23113  minveclem3b  23417  mbfposr  23639  itg2cn  23750  iblcnlem  23775  dvcvx  24003  ulm2  24359  efeq1  24496  dcubic  24793  mcubic  24794  dquart  24800  birthdaylem3  24900  ftalem2  25020  issqf  25082  sqff1o  25128  bposlem7  25235  lgsabs1  25281  gausslemma2dlem1a  25310  lgsquadlem2  25326  dchrisum0lem1  25425  opphllem6  25864  colhp  25882  lmiinv  25904  lmiopp  25914  eupth2lem3lem3  27409  eupth2lem3lem6  27412  nmounbi  27965  ip2eqi  28046  hvmulcan  28263  hvsubcan2  28266  hi2eq  28296  fh2  28812  riesz4i  29256  cvbr4i  29560  xdivpnfrp  29972  isorng  30130  ballotlemfc0  30885  ballotlemfcc  30886  sgnmulsgn  30942  sgnmulsgp  30943  subfacp1lem5  31494  eqfunresadj  31986  sltrec  32250  topfneec2  32677  neibastop3  32683  unccur  33707  cos2h  33715  tan2h  33716  poimirlem25  33749  poimirlem27  33751  dvasin  33810  caures  33869  ismtyima  33915  isdmn3  34186  dmecd  34392  tendospcanN  36805  dochsncom  37164  or3or  38820  neicvgel1  38918  rusbcALT  39140  sbc3orgOLD  39241  climreeq  40326  coseq0  40556  mgmhmpropd  42354
  Copyright terms: Public domain W3C validator