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  5431  aceq1  8823  aceq0  8824  zfac  9165  zfcndac  9320  funcnvmptOLD  28850  axacprim  30838  rp-fakeanorass  36877  rp-fakenanass  36879
 Copyright terms: Public domain W3C validator