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

Theorem bi2anan9r 638
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.)
Hypotheses
Ref Expression
bi2an9.1 (𝜑 → (𝜓𝜒))
bi2an9.2 (𝜃 → (𝜏𝜂))
Assertion
Ref Expression
bi2anan9r ((𝜃𝜑) → ((𝜓𝜏) ↔ (𝜒𝜂)))

Proof of Theorem bi2anan9r
StepHypRef Expression
1 bi2an9.1 . . 3 (𝜑 → (𝜓𝜒))
2 bi2an9.2 . . 3 (𝜃 → (𝜏𝜂))
31, 2bi2anan9 637 . 2 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))
43ancoms 458 1 ((𝜃𝜑) → ((𝜓𝜏) ↔ (𝜒𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  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 206  df-an 396
This theorem is referenced by:  efrn2lp  5654  ltsosr  11103  seqf1olem2  14025  seqf1o  14026  pcval  16798  sltlpss  27807  uspgr2wlkeq  29434  satf0op  34910  fmlafvel  34918  fneval  35759  prtlem5  38256  prjspval  41939  rmydioph  42347  wepwsolem  42378  aomclem8  42397  sprsymrelfolem2  46746
  Copyright terms: Public domain W3C validator