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

Theorem bibi12i 340
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 338 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 bibi2i.1 . . 3 (𝜑𝜓)
43bibi1i 339 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 275 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  575  biadan  818  orbidi  952  pm5.7  953  xorbi12i  1524  xorbi12iOLD  1525  norass  1539  rexbiOLD  3109  vn0  4299  ab0OLD  4336  ab0orv  4339  rexprg  4658  brsymdif  5165  nfnid  5331  asymref  6071  isocnv2  7277  zfcndrep  10551  f1omvdco3  19232  brtxpsd  34482  eliminable-abeqab  35337  bj-sbeq  35371  bj-rcleqf  35499  symrefref3  37029  eldisjn0el  37271  rp-fakeoranass  41793  rp-fakeinunass  41794  relexp0eq  41980  absnsb  45268  ichcom  45658  ichbi12i  45659
  Copyright terms: Public domain W3C validator