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

Theorem bianbi 626
Description: Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023.)
Hypotheses
Ref Expression
bianbi.1 (𝜑 ↔ (𝜓𝜒))
bianbi.2 (𝜓𝜃)
Assertion
Ref Expression
bianbi (𝜑 ↔ (𝜃𝜒))

Proof of Theorem bianbi
StepHypRef Expression
1 bianbi.1 . 2 (𝜑 ↔ (𝜓𝜒))
2 bianbi.2 . . 3 (𝜓𝜃)
32anbi1i 623 . 2 ((𝜓𝜒) ↔ (𝜃𝜒))
41, 3bitri 275 1 (𝜑 ↔ (𝜃𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395
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  df-an 396
This theorem is referenced by:  anbi12i  627  bianassc  642  pm5.53  1005  dfifp4  1067  dfifp5  1068  an3andi  1482  19.28v  1990  19.28  2224  2eu4  2652  r19.26-3  3114  r19.41v  3191  r3ex  3200  3reeanv  3231  r19.41  3264  rmo4  3746  rmo3f  3750  sbc3an  3868  rmo3  3905  difin2  4315  otelxp  5743  dfrefrel5  38421  dfantisymrel4  38665  dfantisymrel5  38666  clnbgrel  47633  grimuhgr  47691
  Copyright terms: Public domain W3C validator