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

Theorem 3bitr2ri 288
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2i.1 (𝜑𝜓)
3bitr2i.2 (𝜒𝜓)
3bitr2i.3 (𝜒𝜃)
Assertion
Ref Expression
3bitr2ri (𝜃𝜑)

Proof of Theorem 3bitr2ri
StepHypRef Expression
1 3bitr2i.1 . . 3 (𝜑𝜓)
2 3bitr2i.2 . . 3 (𝜒𝜓)
31, 2bitr4i 266 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitr2i 264 1 (𝜃𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 195
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 196
This theorem is referenced by:  xorass  1460  ssrab  3643  copsex2gb  5153  relop  5194  dmopab3  5259  restidsing  5377  issref  5428  fununi  5878  dffv2  6181  dfsup2  8233  kmlem3  8857  recmulnq  9665  ovoliunlem1  23077  shne0i  27691  ssiun3  28759  cnvoprab  28886  ind1a  29410  bnj1304  30144  bnj1253  30339  dfrecs2  31227  icorempt2  32375  dalem20  33997  rp-isfinite6  36883  rababg  36898  ssrabf  38329
  Copyright terms: Public domain W3C validator