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

Theorem bi2anan9r 640
 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 639 . 2 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))
43ancoms 463 1 ((𝜃𝜑) → ((𝜓𝜏) ↔ (𝜒𝜂)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400 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 210  df-an 401 This theorem is referenced by:  efrn2lp  5507  ltsosr  10547  seqf1olem2  13453  seqf1o  13454  pcval  16229  uspgr2wlkeq  27527  satf0op  32848  fmlafvel  32856  fneval  34083  prtlem5  36429  prjspval  39932  rmydioph  40321  wepwsolem  40352  aomclem8  40371  sprsymrelfolem2  44371
 Copyright terms: Public domain W3C validator