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  5530  ltsosr  10504  seqf1olem2  13398  seqf1o  13399  pcval  16169  uspgr2wlkeq  27354  satf0op  32521  fmlafvel  32529  fneval  33597  prtlem5  35876  prjspval  39131  rmydioph  39489  wepwsolem  39520  aomclem8  39539  sprsymrelfolem2  43532
  Copyright terms: Public domain W3C validator