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

Theorem bibi1 340
Description: Theorem *4.86 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
bibi1 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))

Proof of Theorem bibi1
StepHypRef Expression
1 id 22 . 2 ((𝜑𝜓) → (𝜑𝜓))
21bibi1d 332 1 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  bitr3  341  bitr  745  eqeq1d  2653  sbeqalb  3521  isclo2  20940  sbc3orgVD  39400  trsbcVD  39427  sbcssgVD  39433  csbingVD  39434  csbsngVD  39443  csbxpgVD  39444  csbrngVD  39446  csbunigVD  39448  csbfv12gALTVD  39449  e2ebindVD  39462
  Copyright terms: Public domain W3C validator