MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr4ri Unicode version

Theorem 3bitr4ri 269
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)
Hypotheses
Ref Expression
3bitr4i.1  |-  ( ph  <->  ps )
3bitr4i.2  |-  ( ch  <->  ph )
3bitr4i.3  |-  ( th  <->  ps )
Assertion
Ref Expression
3bitr4ri  |-  ( th  <->  ch )

Proof of Theorem 3bitr4ri
StepHypRef Expression
1 3bitr4i.2 . 2  |-  ( ch  <->  ph )
2 3bitr4i.1 . . 3  |-  ( ph  <->  ps )
3 3bitr4i.3 . . 3  |-  ( th  <->  ps )
42, 3bitr4i 243 . 2  |-  ( ph  <->  th )
51, 4bitr2i 241 1  |-  ( th  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  pm4.78  565  xor  861  nanbi  1294  nic-ax  1428  2sb5  2051  2sb6  2052  2sb5rf  2056  2sb6rf  2057  moabs  2187  2eu7  2229  2eu8  2230  risset  2590  r19.35  2687  reuind  2968  undif3  3429  unab  3435  inab  3436  inssdif0  3521  ssundif  3537  snss  3748  pwtp  3824  unipr  3841  uni0b  3852  iinuni  3985  pwtr  4226  elxp2  4707  opthprc  4736  xpiundir  4744  elvvv  4749  xpsspwOLD  4798  relun  4802  inopab  4816  difopab  4817  ralxpf  4830  dmiun  4887  rniun  5091  cnvresima  5162  imaco  5178  fnopabg  5367  dff1o2  5477  fnsuppres  5732  idref  5759  opabex3  5769  imaiun  5771  ovmptss  6200  sorpss  6282  rankc1  7542  aceq1  7744  dfac10  7763  fin41  8070  axgroth6  8450  genpass  8633  infm3  9713  prime  10092  elixx3g  10669  elfz2  10789  elfzuzb  10792  rpnnen2  12504  divalgb  12603  1nprm  12763  maxprmfct  12792  vdwmc  13025  imasleval  13443  issubm  14425  issubg3  14637  efgrelexlemb  15059  ist1-2  17075  elflim2  17659  isfcls  17704  istlm  17867  isnlm  18186  ishl2  18787  h1de2ctlem  22134  nonbooli  22230  5oalem7  22239  ho01i  22408  rnbra  22687  cvnbtwn3  22868  chrelat2i  22945  ballotlem2  23047  mptfnf  23226  iscvm  23790  untuni  24055  dfso3  24074  dffr5  24110  nofulllem5  24360  brtxpsd3  24436  brbigcup  24438  fixcnv  24448  ellimits  24450  brimage  24465  brcart  24471  brimg  24476  brapply  24477  brcup  24478  brcap  24479  dfrdg4  24488  ellines  24775  anddi2  24941  elicc3  26228  iscrngo2  26623  prtlem70  26715  prtlem100  26721  n0el  26725  prtlem15  26743  prter2  26749  ralxpxfr2d  26760  inisegn0  27140  aaitgo  27367  isdomn3  27523  2sbc6g  27615  2sbc5g  27616  2reu7  27969  2reu8  27970  bnj976  28809  bnj1185  28826  bnj543  28925  bnj571  28938  bnj611  28950  bnj916  28965  bnj1000  28973  bnj1040  29002  a12study9  29120  lcvnbtwn3  29218  ishlat1  29542  ishlat2  29543  hlrelat2  29592  islpln5  29724  islvol5  29768  pclclN  30080  cdleme0nex  30479
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator