Theorem bi2anan9 571

Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)

Hypotheses

Ref	Expression
bi2an9.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bi2an9.2	⊢ (𝜃 → (𝜏 ↔ 𝜂))

Assertion

Ref	Expression
bi2anan9	⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Proof of Theorem bi2anan9

Step	Hyp	Ref	Expression
1		bi2an9.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	anbi1d 453	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜏)))
3		bi2an9.2	. . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂))
4	3	anbi2d 452	. 2 ⊢ (𝜃 → ((𝜒 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
5	2, 4	sylan9bb 450	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bi2anan9r  572  rspc2gv  2722  ralprg  3467  raltpg  3469  prssg  3568  prsspwg  3570  opelopab2a  4056  opelxp  4430  eqrel  4485  eqrelrel  4497  brcog  4561  dff13  5487  resoprab2  5677  ovig  5701  dfoprab4f  5898  f1o2ndf1  5928  eroveu  6313  th3qlem1  6324  th3qlem2  6325  th3q  6327  oviec  6328  endisj  6470  dfplpq2  6816  dfmpq2  6817  ordpipqqs  6836  enq0enq  6893  mulnnnq0  6912  ltsrprg  7196  axcnre  7319  axmulgt0  7461  addltmul  8544  ltxr  9141  sumsqeq0  9870  dvds2lem  10588  opoe  10675  omoe  10676  opeo  10677  omeo  10678  gcddvds  10735  dfgcd2  10783