Theorem bi2anan9 595

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bi2anan9r  596  rspc2gv  2801  ralprg  3574  raltpg  3576  prssg  3677  prsspwg  3679  opelopab2a  4187  opelxp  4569  eqrel  4628  eqrelrel  4640  brcog  4706  dff13  5669  resoprab2  5868  ovig  5892  dfoprab4f  6091  f1o2ndf1  6125  eroveu  6520  th3qlem1  6531  th3qlem2  6532  th3q  6534  oviec  6535  endisj  6718  dfplpq2  7165  dfmpq2  7166  ordpipqqs  7185  enq0enq  7242  mulnnnq0  7261  ltsrprg  7558  axcnre  7692  axmulgt0  7839  addltmul  8959  ltxr  9565  sumsqeq0  10374  mul0inf  11015  dvds2lem  11508  opoe  11595  omoe  11596  opeo  11597  omeo  11598  gcddvds  11655  dfgcd2  11705  txbasval  12439  cnmpt12  12459  cnmpt22  12466