Theorem bi2anan9 638

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	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bi2an9.2	. 2 ⊢ (𝜃 → (𝜏 ↔ 𝜂))
3		pm4.38 637	. 2 ⊢ (((𝜓 ↔ 𝜒) ∧ (𝜏 ↔ 𝜂)) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
4	1, 2, 3	syl2an 596	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  bi2anan9r  639  rspc2gv  3595  2reu5  3726  ralprgf  4654  ralprg  4656  raltpg  4658  prssg  4779  prsspwg  4783  ssprss  4784  intprg  4941  opelopab2a  5490  opelxp  5667  eqrel  5738  eqrelrel  5751  brcog  5820  tpres  7157  dff13  7211  cbvmpov  7464  resoprab2  7488  ovig  7515  dfoprab4f  8014  f1o2ndf1  8078  om00el  8517  oeoe  8540  eroveu  8762  endisj  9005  infxpen  9943  dfac5lem4OLD  10057  sornom  10206  ltsrpr  11006  axcnre  11093  axmulgt0  11224  wloglei  11686  mulge0b  12029  addltmul  12394  ltxr  13051  fzadd2  13496  sumsqeq0  14120  ccat0  14517  rlim  15437  cpnnen  16173  dvds2lem  16214  opoe  16309  omoe  16310  opeo  16311  omeo  16312  gcddvds  16449  dfgcd2  16492  pcqmul  16800  xpsfrnel2  17503  eqgval  19091  frgpuplem  19686  mpfind  22047  2ndcctbss  23375  txbasval  23526  cnmpt12  23587  cnmpt22  23594  prdsxmslem2  24450  ishtpy  24904  bcthlem1  25257  bcth  25262  volun  25479  vitali  25547  itg1addlem3  25632  rolle  25927  mumullem2  27123  lgsquadlem3  27326  lgsquad  27327  2sqlem7  27368  scutval  27746  slerec  27765  remulscllem2  28405  axpasch  28921  wlkson  29635  iswwlksnon  29833  wpthswwlks2on  29941  eulplig  30464  hlimi  31167  leopadd  32111  tpssg  32516  brab2d  32585  eqrelrd2  32594  cntzun  33051  isinftm  33150  finexttrb  33653  metidv  33875  satfv1  35343  satfbrsuc  35346  gonarlem  35374  satfv0fvfmla0  35393  satfv1fvfmla1  35403  altopthg  35948  altopthbg  35949  brsegle  36089  bj-imdirvallem  37161  finxpreclem3  37374  itg2addnclem3  37660  exan3  38275  exanres  38276  exanres3  38277  eqrel2  38280  brcoss  38415  brcoss3  38417  brcoels  38419  br1cossxrnres  38432  brcosscnv  38456  prtlem13  38854  dib1dim  41152  f1o2d2  42214  pellex  42816  tfsconcatb0  43326  tfsconcat00  43329  prsprel  47481  uspgrsprf1  48128  uspgrsprfo  48129  brab2ddw2  48811