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

Theorem 3bitr4ri 271
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 245 . 2  |-  ( ph  <->  th )
51, 4bitr2i 243 1  |-  ( th  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  pm4.78  567  xor  863  nanbi  1304  nic-ax  1448  2sb5  2189  2sb6  2190  2sb5rf  2195  2sb6rf  2196  moabs  2326  2eu7  2368  2eu8  2369  risset  2754  r19.35  2856  reuind  3138  undif3  3603  unab  3609  inab  3610  inssdif0  3696  ssundif  3712  snss  3927  pwtp  4013  unipr  4030  uni0b  4041  iinuni  4175  pwtr  4417  reusv2lem4  4728  elxp2  4897  opthprc  4926  xpiundir  4934  elvvv  4938  xpsspwOLD  4988  relun  4992  inopab  5006  difopab  5007  ralxpf  5020  dmiun  5079  rniun  5283  cnvresima  5360  imaco  5376  fnopabg  5569  dff1o2  5680  brprcneu  5722  fnsuppres  5953  idref  5980  opabex3d  5990  opabex3  5991  imaiun  5993  ovmptss  6429  sorpss  6528  rankc1  7797  aceq1  7999  dfac10  8018  fin41  8325  axgroth6  8704  genpass  8887  infm3  9968  prime  10351  elixx3g  10930  elfz2  11051  elfzuzb  11054  rpnnen2  12826  divalgb  12925  1nprm  13085  maxprmfct  13114  vdwmc  13347  imasleval  13767  issubm  14749  issubg3  14961  efgrelexlemb  15383  ist1-2  17412  elflim2  17997  isfcls  18042  istlm  18215  isnlm  18712  ishl2  19325  0wlk  21546  0trl  21547  h1de2ctlem  23058  nonbooli  23154  5oalem7  23163  ho01i  23332  rnbra  23611  cvnbtwn3  23792  chrelat2i  23869  disjex  24033  mptfnf  24074  ballotlem2  24747  iscvm  24947  untuni  25159  dfso3  25178  dffr5  25377  nofulllem5  25662  brtxpsd3  25742  brbigcup  25744  fixcnv  25754  ellimits  25756  elfuns  25761  brimage  25772  brcart  25778  brimg  25783  brapply  25784  brcup  25785  brcap  25786  dfrdg4  25796  dfint3  25798  ellines  26087  mblfinlem2  26245  elicc3  26321  iscrngo2  26609  prtlem70  26699  prtlem100  26705  n0el  26709  prtlem15  26725  prter2  26731  ralxpxfr2d  26742  inisegn0  27119  aaitgo  27345  isdomn3  27501  2sbc6g  27593  2sbc5g  27594  2reu7  27946  2reu8  27947  raldifsnb  28059  bnj976  29149  bnj1185  29166  bnj543  29265  bnj571  29278  bnj611  29290  bnj916  29305  bnj1000  29313  bnj1040  29342  2sb5NEW7  29610  2sb6NEW7  29611  2sb5rfOLD7  29762  2sb6rfOLD7  29763  lcvnbtwn3  29827  ishlat1  30151  ishlat2  30152  hlrelat2  30201  islpln5  30333  islvol5  30377  pclclN  30689  cdleme0nex  31088
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 179
  Copyright terms: Public domain W3C validator