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

Theorem 3bitr3ri 276
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
3bitr3i.1
3bitr3i.2
3bitr3i.3
Assertion
Ref Expression
3bitr3ri

Proof of Theorem 3bitr3ri
StepHypRef Expression
1 3bitr3i.3 . 2
2 3bitr3i.1 . . 3
3 3bitr3i.2 . . 3
42, 3bitr3i 251 . 2
51, 4bitr3i 251 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  bigolden  935  2eu8  2386  2ralor  3027  sbcco  3350  dfiin2g  4363  zfpair  4689  dffun6f  5607  fsplit  6905  axdc3lem4  8854  istrkg2ld  23858  legso  23985  disjunsn  27453  gtiso  27519  fpwrelmapffslem  27555  qqhre  27998  dfpo2  29184  dfdm5  29206  dfrn5  29207  nofulllem5  29466  symdifass  29477  brimg  29587  elnev  31345  2reu8  32197  cdlemefrs29bpre0  36122  cdlemftr3  36291
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 185
  Copyright terms: Public domain W3C validator