Theorem bi2anan9 606

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 465	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜏)))
3		bi2an9.2	. . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂))
4	3	anbi2d 464	. 2 ⊢ (𝜃 → ((𝜒 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
5	2, 4	sylan9bb 462	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bi2anan9r  607  rspc2gv  2853  ralprg  3643  raltpg  3645  prssg  3749  prsspwg  3752  opelopab2a  4265  opelxp  4656  eqrel  4715  eqrelrel  4727  brcog  4794  dff13  5768  resoprab2  5971  ovig  5995  dfoprab4f  6193  f1o2ndf1  6228  eroveu  6625  th3qlem1  6636  th3qlem2  6637  th3q  6639  oviec  6640  endisj  6823  exmidapne  7258  dfplpq2  7352  dfmpq2  7353  ordpipqqs  7372  enq0enq  7429  mulnnnq0  7448  ltsrprg  7745  axcnre  7879  axmulgt0  8028  addltmul  9154  ltxr  9774  sumsqeq0  10598  mul0inf  11248  dvds2lem  11809  opoe  11899  omoe  11900  opeo  11901  omeo  11902  gcddvds  11963  dfgcd2  12014  pcqmul  12302  xpsfrnel2  12764  eqgval  13080  txbasval  13737  cnmpt12  13757  cnmpt22  13764  2sqlem7  14438