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

Theorem bibi12i 338
Description: The equivalence of two equivalences. (Contributed by NM, 26-May-1993.)
Hypotheses
Ref Expression
bibi2i.1 (𝜑𝜓)
bibi12i.2 (𝜒𝜃)
Assertion
Ref Expression
bibi12i ((𝜑𝜒) ↔ (𝜓𝜃))

Proof of Theorem bibi12i
StepHypRef Expression
1 bibi12i.2 . . 3 (𝜒𝜃)
21bibi2i 336 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 bibi2i.1 . . 3 (𝜑𝜓)
43bibi1i 337 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 274 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  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:  pm5.32  572  biadan  817  orbidi  950  pm5.7  951  xorbi12i  1518  norass  1531  rexbiOLD  3095  vn0  4338  ab0OLD  4373  ab0orv  4376  rexprg  4695  brsymdif  5204  nfnid  5371  asymref  6120  isocnv2  7335  zfcndrep  10648  f1omvdco3  19443  brtxpsd  35731  eliminable-abeqab  36586  bj-sbeq  36620  bj-rcleqf  36745  symrefref3  38275  eldisjn0el  38517  abbibw  42370  rp-fakeoranass  43218  rp-fakeinunass  43219  relexp0eq  43405  absnsb  46678  ichcom  47067  ichbi12i  47068
  Copyright terms: Public domain W3C validator