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  2064  2sb6  2065  2sb5rf  2069  2sb6rf  2070  moabs  2200  2eu7  2242  2eu8  2243  risset  2603  r19.35  2700  reuind  2981  undif3  3442  unab  3448  inab  3449  inssdif0  3534  ssundif  3550  snss  3761  pwtp  3840  unipr  3857  uni0b  3868  iinuni  4001  pwtr  4242  elxp2  4723  opthprc  4752  xpiundir  4760  elvvv  4765  xpsspwOLD  4814  relun  4818  inopab  4832  difopab  4833  ralxpf  4846  dmiun  4903  rniun  5107  cnvresima  5178  imaco  5194  fnopabg  5383  dff1o2  5493  fnsuppres  5748  idref  5775  opabex3  5785  imaiun  5787  ovmptss  6216  sorpss  6298  rankc1  7558  aceq1  7760  dfac10  7779  fin41  8086  axgroth6  8466  genpass  8649  infm3  9729  prime  10108  elixx3g  10685  elfz2  10805  elfzuzb  10808  rpnnen2  12520  divalgb  12619  1nprm  12779  maxprmfct  12808  vdwmc  13041  imasleval  13459  issubm  14441  issubg3  14653  efgrelexlemb  15075  ist1-2  17091  elflim2  17675  isfcls  17720  istlm  17883  isnlm  18202  ishl2  18803  h1de2ctlem  22150  nonbooli  22246  5oalem7  22255  ho01i  22424  rnbra  22703  cvnbtwn3  22884  chrelat2i  22961  ballotlem2  23063  mptfnf  23241  iscvm  23805  untuni  24070  dfso3  24089  dffr5  24181  nofulllem5  24431  brtxpsd3  24507  brbigcup  24509  fixcnv  24519  ellimits  24521  brimage  24536  brcart  24542  brimg  24547  brapply  24548  brcup  24549  brcap  24550  dfrdg4  24560  ellines  24847  anddi2  25044  elicc3  26331  iscrngo2  26726  prtlem70  26818  prtlem100  26824  n0el  26828  prtlem15  26846  prter2  26852  ralxpxfr2d  26863  inisegn0  27243  aaitgo  27470  isdomn3  27626  2sbc6g  27718  2sbc5g  27719  2reu7  28072  2reu8  28073  opabex3d  28190  0wlk  28343  0trl  28344  bnj976  29125  bnj1185  29142  bnj543  29241  bnj571  29254  bnj611  29266  bnj916  29281  bnj1000  29289  bnj1040  29318  2sb5NEW7  29581  2sb6NEW7  29582  2sb5rfOLD7  29717  2sb6rfOLD7  29718  a12study9  29742  lcvnbtwn3  29840  ishlat1  30164  ishlat2  30165  hlrelat2  30214  islpln5  30346  islvol5  30390  pclclN  30702  cdleme0nex  31101
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