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

Theorem bi2anan9r 636
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 635 . 2 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))
43ancoms 459 1 ((𝜃𝜑) → ((𝜓𝜏) ↔ (𝜒𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  efrn2lp  5425  ltsosr  10362  seqf1olem2  13260  seqf1o  13261  pcval  16010  uspgr2wlkeq  27110  satf0op  32232  fmlafvel  32240  fneval  33309  prtlem5  35527  prjspval  38750  rmydioph  39096  wepwsolem  39127  aomclem8  39146  sprsymrelfolem2  43137
  Copyright terms: Public domain W3C validator