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

Theorem bibi12i 343
 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 341 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 bibi2i.1 . . 3 (𝜑𝜓)
43bibi1i 342 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 278 1 ((𝜑𝜒) ↔ (𝜓𝜃))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209 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 210 This theorem is referenced by:  pm5.32  577  biadan  818  orbidi  950  pm5.7  951  xorbi12i  1516  xorbi12iOLD  1517  norass  1534  norassOLD  1535  abbiOLD  2892  rexbi  3169  vn0  4237  ab0  4272  ab0orv  4275  brsymdif  5091  nfnid  5244  asymref  5948  isocnv2  7078  zfcndrep  10074  f1omvdco3  18644  brtxpsd  33745  eliminable-abeqab  34587  bj-sbeq  34622  bj-rcleqf  34742  symrefref3  36240  rp-fakeoranass  40595  rp-fakeinunass  40596  relexp0eq  40775  absnsb  43985  ichcom  44344  ichbi12i  44345
 Copyright terms: Public domain W3C validator