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

Theorem bibi1 350
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 342 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  351  bitr  803  eqeq1d  2728  sbeqalb  3844  isclo2  23083  sbc3orgVD  44527  trsbcVD  44553  sbcssgVD  44559  csbingVD  44560  csbsngVD  44569  csbxpgVD  44570  csbrngVD  44572  csbunigVD  44574  csbfv12gALTVD  44575  e2ebindVD  44588
  Copyright terms: Public domain W3C validator