Theorem bi2anan9 917

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  bi2anan9r  918  rspc2gv  3321  2reu5  3416  ralprg  4234  raltpg  4236  prssg  4350  prsspwg  4355  ssprss  4356  opelopab2a  4990  opelxp  5146  eqrel  5209  eqrelrel  5221  brcog  5288  tpres  6466  dff13  6512  resoprab2  6757  ovig  6782  dfoprab4f  7226  f1o2ndf1  7285  om00el  7656  oeoe  7679  eroveu  7842  endisj  8047  infxpen  8837  dfac5lem4  8949  sornom  9099  ltsrpr  9898  axcnre  9985  axmulgt0  10112  wloglei  10560  mulge0b  10893  addltmul  11268  ltxr  11949  fzadd2  12376  sumsqeq0  12942  rlim  14226  cpnnen  14958  dvds2lem  14994  opoe  15087  omoe  15088  opeo  15089  omeo  15090  gcddvds  15225  dfgcd2  15263  pcqmul  15558  xpsfrnel2  16225  eqgval  17643  frgpuplem  18185  mpfind  19536  2ndcctbss  21258  txbasval  21409  cnmpt12  21470  cnmpt22  21477  prdsxmslem2  22334  ishtpy  22771  bcthlem1  23121  bcth  23126  volun  23313  vitali  23382  itg1addlem3  23465  rolle  23753  mumullem2  24906  lgsquadlem3  25107  lgsquad  25108  2sqlem7  25149  axpasch  25821  wlkson  26552  iswwlksnon  26740  numclwwlkovg  27220  numclwwlkovh  27234  eulplig  27337  hlimi  28045  leopadd  28991  eqrelrd2  29426  isinftm  29735  metidv  29935  scutval  31911  slerec  31923  altopthg  32074  altopthbg  32075  brsegle  32215  finxpreclem3  33230  itg2addnclem3  33463  exan3  34062  exanres  34063  exanres3  34064  eqrel2  34068  prtlem13  34153  dib1dim  36454  pellex  37399  prsprel  41737  uspgrsprf1  41755  uspgrsprfo  41756