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

Theorem bibi1i 327
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 211 . 2 ((𝜑𝜒) ↔ (𝜒𝜑))
2 bibi2i.1 . . 3 (𝜑𝜓)
32bibi2i 326 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 bicom 211 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 285 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 195
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 196
This theorem is referenced by:  bibi12i  328  biluk  970  xorass  1460  hadbi  1528  hadnot  1532  sbrbis  2393  ssequn1  3745  symdifass  3815  asymref  5418  aceq1  8801  aceq0  8802  zfac  9143  zfcndac  9298  funcnvmptOLD  28644  axacprim  30632  rp-fakeanorass  36671  rp-fakenanass  36673
  Copyright terms: Public domain W3C validator