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

Theorem bibi1i 343
 Description: Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
bibi2i.1 (𝜑𝜓)
Assertion
Ref Expression
bibi1i ((𝜑𝜒) ↔ (𝜓𝜒))

Proof of Theorem bibi1i
StepHypRef Expression
1 bicom 225 . 2 ((𝜑𝜒) ↔ (𝜒𝜑))
2 bibi2i.1 . . 3 (𝜑𝜓)
32bibi2i 342 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 bicom 225 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 301 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:  bibi12i  344  biluk  391  biadaniALT  821  nanass  1502  xorass  1508  hadbi  1600  hadcoma  1601  hadnot  1605  sbrbis  2316  ssequn1  4086  asymref  5946  aceq1  9567  aceq0  9568  zfac  9910  zfcndac  10069  hashreprin  32109  axacprim  33154  eliminable-abeqv  34576  wl-3xorcoma  35165  wl-3xornot  35168  redundpbi1  36296  rp-fakeanorass  40584  ichn  44331  dfich2  44333
 Copyright terms: Public domain W3C validator