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

Theorem bi2anan9r 639
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 638 . 2 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))
43ancoms 458 1 ((𝜃𝜑) → ((𝜓𝜏) ↔ (𝜒𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  efrn2lp  5670  ltsosr  11132  seqf1olem2  14080  seqf1o  14081  pcval  16878  sltlpss  27960  uspgr2wlkeq  29679  satf0op  35362  fmlafvel  35370  fneval  36335  prtlem5  38842  prjspval  42590  rmydioph  43003  wepwsolem  43031  aomclem8  43050  sprsymrelfolem2  47418
  Copyright terms: Public domain W3C validator