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

Theorem bibi1 352
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 344 1 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  bitr3  353  bitr  804  eqeq1d  2739  sbeqalb  3808  isclo2  22442  sbc3orgVD  43140  trsbcVD  43166  sbcssgVD  43172  csbingVD  43173  csbsngVD  43182  csbxpgVD  43183  csbrngVD  43185  csbunigVD  43187  csbfv12gALTVD  43188  e2ebindVD  43201
  Copyright terms: Public domain W3C validator