Theorem bi2anan9 639

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 638	. 2 ⊢ (((𝜓 ↔ 𝜒) ∧ (𝜏 ↔ 𝜂)) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
4	1, 2, 3	syl2an 599	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  bi2anan9r  640  rspc2gv  3546  2reu5  3671  ralprgf  4608  ralprg  4610  raltpg  4614  prssg  4732  prsspwg  4736  ssprss  4737  intprg  4892  opelopab2a  5416  opelxp  5587  eqrel  5655  eqrelrel  5667  brcog  5735  tpres  7016  dff13  7067  resoprab2  7329  ovig  7355  dfoprab4f  7826  f1o2ndf1  7891  om00el  8304  oeoe  8327  eroveu  8494  endisj  8732  infxpen  9628  dfac5lem4  9740  sornom  9891  ltsrpr  10691  axcnre  10778  axmulgt0  10907  wloglei  11364  mulge0b  11702  addltmul  12066  ltxr  12707  fzadd2  13147  sumsqeq0  13748  ccat0  14132  rlim  15056  cpnnen  15790  dvds2lem  15830  opoe  15924  omoe  15925  opeo  15926  omeo  15927  gcddvds  16062  dfgcd2  16106  pcqmul  16406  xpsfrnel2  17069  eqgval  18593  frgpuplem  19162  mpfind  21067  2ndcctbss  22352  txbasval  22503  cnmpt12  22564  cnmpt22  22571  prdsxmslem2  23427  ishtpy  23869  bcthlem1  24221  bcth  24226  volun  24442  vitali  24510  itg1addlem3  24595  rolle  24887  mumullem2  26062  lgsquadlem3  26263  lgsquad  26264  2sqlem7  26305  axpasch  27032  wlkson  27744  iswwlksnon  27937  wpthswwlks2on  28045  eulplig  28566  hlimi  29269  leopadd  30213  eqrelrd2  30675  cntzun  31039  isinftm  31154  finexttrb  31451  metidv  31556  satfv1  33038  satfbrsuc  33041  gonarlem  33069  satfv0fvfmla0  33088  satfv1fvfmla1  33098  scutval  33731  slerec  33750  altopthg  34006  altopthbg  34007  brsegle  34147  bj-imdirvallem  35086  finxpreclem3  35301  itg2addnclem3  35567  exan3  36166  exanres  36167  exanres3  36168  eqrel2  36172  brcoss  36291  brcoss3  36293  brcoels  36295  br1cossxrnres  36303  brcosscnv  36327  prtlem13  36619  dib1dim  38916  pellex  40360  prsprel  44612  uspgrsprf1  44982  uspgrsprfo  44983