Theorem bi2anan9 913

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  bi2anan9r  914  2reu5  3383  ralprg  4181  raltpg  4183  prssg  4290  prsspwg  4295  ssprss  4296  opelopab2a  4915  opelxp  5070  eqrel  5132  eqrelrel  5144  brcog  5210  tpres  6371  dff13  6416  resoprab2  6655  ovig  6680  dfoprab4f  7117  f1o2ndf1  7172  om00el  7543  oeoe  7566  eroveu  7729  endisj  7932  infxpen  8720  dfac5lem4  8832  sornom  8982  ltsrpr  9777  axcnre  9864  axmulgt0  9991  wloglei  10439  mulge0b  10772  addltmul  11145  ltxr  11825  fzadd2  12247  sumsqeq0  12804  rlim  14074  cpnnen  14797  dvds2lem  14832  opoe  14925  omoe  14926  opeo  14927  omeo  14928  gcddvds  15063  dfgcd2  15101  pcqmul  15396  xpsfrnel2  16048  eqgval  17466  frgpuplem  18008  mpfind  19357  2ndcctbss  21068  txbasval  21219  cnmpt12  21280  cnmpt22  21287  prdsxmslem2  22144  ishtpy  22579  bcthlem1  22929  bcth  22934  volun  23120  vitali  23188  itg1addlem3  23271  rolle  23557  mumullem2  24706  lgsquadlem3  24907  lgsquad  24908  2sqlem7  24949  axpasch  25621  usgra2adedgwlkonALT  26144  usgra2wlkspthlem1  26147  el2wlkonotot1  26401  frg2wot1  26584  frg2woteqm  26586  numclwwlkovg  26614  hlimi  27429  leopadd  28375  eqrelrd2  28806  isinftm  29066  metidv  29263  altopthg  31244  altopthbg  31245  brsegle  31385  finxpreclem3  32406  itg2addnclem3  32633  prtlem13  33171  dib1dim  35472  pellex  36417  wlkson  40864  iswwlksnon  41051  frgr2wwlk1  41494  av-numclwwlkovg  41518  av-numclwwlkovh  41531