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

Theorem bibi1 351
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 343 1 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
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 207
This theorem is referenced by:  bitr3  352  bitr  805  eqeq1d  2737  sbeqalb  3859  isclo2  23112  sbc3orgVD  44849  trsbcVD  44875  sbcssgVD  44881  csbingVD  44882  csbsngVD  44891  csbxpgVD  44892  csbrngVD  44894  csbunigVD  44896  csbfv12gALTVD  44897  e2ebindVD  44910
  Copyright terms: Public domain W3C validator