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  3582  2reu5  3712  ralprgf  4644  ralprg  4646  raltpg  4648  prssg  4768  prsspwg  4772  ssprss  4773  intprg  4929  opelopab2a  5473  opelxp  5650  eqrel  5723  eqrelrel  5736  brcog  5805  tpres  7135  dff13  7188  cbvmpov  7441  resoprab2  7465  ovig  7492  dfoprab4f  7988  f1o2ndf1  8052  om00el  8491  oeoe  8514  eroveu  8736  endisj  8977  infxpen  9905  dfac5lem4OLD  10019  sornom  10168  ltsrpr  10968  axcnre  11055  axmulgt0  11187  wloglei  11649  mulge0b  11992  addltmul  12357  ltxr  13014  fzadd2  13459  sumsqeq0  14086  ccat0  14483  rlim  15402  cpnnen  16138  dvds2lem  16179  opoe  16274  omoe  16275  opeo  16276  omeo  16277  gcddvds  16414  dfgcd2  16457  pcqmul  16765  xpsfrnel2  17468  eqgval  19089  frgpuplem  19684  mpfind  22042  2ndcctbss  23370  txbasval  23521  cnmpt12  23582  cnmpt22  23589  prdsxmslem2  24444  ishtpy  24898  bcthlem1  25251  bcth  25256  volun  25473  vitali  25541  itg1addlem3  25626  rolle  25921  mumullem2  27117  lgsquadlem3  27320  lgsquad  27321  2sqlem7  27362  scutval  27741  slerec  27760  remulscllem2  28403  axpasch  28919  wlkson  29633  iswwlksnon  29831  wpthswwlks2on  29942  eulplig  30465  hlimi  31168  leopadd  32112  tpssg  32517  brab2d  32588  eqrelrd2  32599  cntzun  33048  isinftm  33150  finexttrb  33678  metidv  33905  satfv1  35407  satfbrsuc  35410  gonarlem  35438  satfv0fvfmla0  35457  satfv1fvfmla1  35467  altopthg  36011  altopthbg  36012  brsegle  36152  bj-imdirvallem  37224  finxpreclem3  37437  itg2addnclem3  37723  exan3  38342  exanres  38343  exanres3  38344  eqrel2  38347  sucmapleftuniq  38512  brcoss  38543  brcoss3  38545  brcoels  38547  br1cossxrnres  38560  brcosscnv  38584  prtlem13  38977  dib1dim  41274  f1o2d2  42336  pellex  42938  tfsconcatb0  43447  tfsconcat00  43450  prsprel  47597  uspgrsprf1  48257  uspgrsprfo  48258  brab2ddw2  48940