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

Theorem bibi1 343
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 335 1 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198
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 199
This theorem is referenced by:  bitr3  344  bitr  841  eqeq1d  2827  sbeqalb  3715  isclo2  21263  sbc3orgVD  39905  trsbcVD  39931  sbcssgVD  39937  csbingVD  39938  csbsngVD  39947  csbxpgVD  39948  csbrngVD  39950  csbunigVD  39952  csbfv12gALTVD  39953  e2ebindVD  39966
  Copyright terms: Public domain W3C validator