Theorem bi2anan9 644

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  bi2anan9r  645  rspc2gv  3570  2reu5  3699  ralprgf  4627  ralprg  4629  raltpg  4631  prssg  4751  prsspwg  4755  ssprss  4756  intprg  4912  opelopab2a  5478  opelxp  5655  eqrel  5728  eqrelrel  5741  brcog  5809  tpres  7146  dff13  7199  cbvmpov  7452  resoprab2  7476  ovig  7503  dfoprab4f  7999  f1o2ndf1  8062  mpof1o2d  8066  om00el  8502  oeoe  8526  eroveu  8750  endisj  8993  infxpen  9928  dfac5lem4OLD  10042  sornom  10191  ltsrpr  10992  axcnre  11079  axmulgt0  11212  wloglei  11674  mulge0b  12018  addltmul  12405  ltxr  13058  fzadd2  13505  sumsqeq0  14133  ccat0  14530  rlim  15449  cpnnen  16188  dvds2lem  16229  opoe  16324  omoe  16325  opeo  16326  omeo  16327  gcddvds  16464  dfgcd2  16507  pcqmul  16816  xpsfrnel2  17520  eqgval  19144  frgpuplem  19739  mpfind  22092  2ndcctbss  23439  txbasval  23590  cnmpt12  23651  cnmpt22  23658  prdsxmslem2  24513  ishtpy  24958  bcthlem1  25310  bcth  25315  volun  25531  vitali  25599  itg1addlem3  25684  rolle  25976  mumullem2  27162  lgsquadlem3  27364  lgsquad  27365  2sqlem7  27406  cutsval  27791  lesrec  27810  remulscllem2  28512  axpasch  29029  wlkson  29742  iswwlksnon  29940  wpthswwlks2on  30051  eulplig  30575  hlimi  31278  leopadd  32222  tpssg  32626  brab2d  32698  eqrelrd2  32709  cntzun  33161  isinftm  33263  finexttrb  33858  metidv  34085  satfv1  35600  satfbrsuc  35603  gonarlem  35631  satfv0fvfmla0  35650  satfv1fvfmla1  35660  altopthg  36204  altopthbg  36205  brsegle  36345  bj-imdirvallem  37549  finxpreclem3  37764  itg2addnclem3  38049  exan3  38676  exanres  38677  exanres3  38678  eqrel2  38681  sucmapleftuniq  38866  brcoss  38897  brcoss3  38899  brcoels  38901  br1cossxrnres  38914  brcosscnv  38938  disjimeceqim2  39181  eldisjim3  39191  prtlem13  39369  dib1dim  41666  pellex  43289  tfsconcatb0  43798  tfsconcat00  43801  prsprel  47970  uspgrsprf1  48646  uspgrsprfo  48647  brab2ddw2  49328