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  2889  ralprg  3684  raltpg  3686  prssg  3790  prsspwg  3793  opelopab2a  4311  opelxp  4705  eqrel  4764  eqrelrel  4776  brcog  4845  dff13  5837  resoprab2  6042  ovig  6067  dfoprab4f  6279  f1o2ndf1  6314  eroveu  6713  th3qlem1  6724  th3qlem2  6725  th3q  6727  oviec  6728  endisj  6919  exmidapne  7372  dfplpq2  7467  dfmpq2  7468  ordpipqqs  7487  enq0enq  7544  mulnnnq0  7563  ltsrprg  7860  axcnre  7994  axmulgt0  8144  addltmul  9274  ltxr  9897  sumsqeq0  10763  ccat0  11052  mul0inf  11552  dvds2lem  12114  opoe  12206  omoe  12207  opeo  12208  omeo  12209  gcddvds  12284  dfgcd2  12335  pcqmul  12626  xpsfrnel2  13178  eqgval  13559  txbasval  14739  cnmpt12  14759  cnmpt22  14766  lgsquadlem3  15556  lgsquad  15557  2sqlem7  15598