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

Theorem bibi12i 339
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 337 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 bibi2i.1 . . 3 (𝜑𝜓)
43bibi1i 338 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 275 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  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:  pm5.32  573  biadan  819  orbidi  955  pm5.7  956  xorbi12i  1524  norass  1537  rexbiOLD  3105  vn0  4345  ab0orv  4383  rexprg  4697  brsymdif  5202  nfnid  5375  asymref  6136  isocnv2  7351  zfcndrep  10654  f1omvdco3  19467  brtxpsd  35895  eliminable-abeqab  36869  bj-sbeq  36902  bj-rcleqf  37026  symrefref3  38565  eldisjn0el  38807  abbibw  42687  rp-fakeoranass  43527  rp-fakeinunass  43528  relexp0eq  43714  absnsb  47039  ichcom  47446  ichbi12i  47447
  Copyright terms: Public domain W3C validator