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  3587  2reu5  3718  ralprgf  4646  ralprg  4648  raltpg  4650  prssg  4770  prsspwg  4774  ssprss  4775  intprg  4931  opelopab2a  5478  opelxp  5655  eqrel  5727  eqrelrel  5740  brcog  5809  tpres  7137  dff13  7191  cbvmpov  7444  resoprab2  7468  ovig  7495  dfoprab4f  7991  f1o2ndf1  8055  om00el  8494  oeoe  8517  eroveu  8739  endisj  8981  infxpen  9908  dfac5lem4OLD  10022  sornom  10171  ltsrpr  10971  axcnre  11058  axmulgt0  11190  wloglei  11652  mulge0b  11995  addltmul  12360  ltxr  13017  fzadd2  13462  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  19056  frgpuplem  19651  mpfind  22012  2ndcctbss  23340  txbasval  23491  cnmpt12  23552  cnmpt22  23559  prdsxmslem2  24415  ishtpy  24869  bcthlem1  25222  bcth  25227  volun  25444  vitali  25512  itg1addlem3  25597  rolle  25892  mumullem2  27088  lgsquadlem3  27291  lgsquad  27292  2sqlem7  27333  scutval  27711  slerec  27730  remulscllem2  28370  axpasch  28886  wlkson  29600  iswwlksnon  29798  wpthswwlks2on  29906  eulplig  30429  hlimi  31132  leopadd  32076  tpssg  32481  brab2d  32552  eqrelrd2  32561  cntzun  33022  isinftm  33124  finexttrb  33638  metidv  33865  satfv1  35346  satfbrsuc  35349  gonarlem  35377  satfv0fvfmla0  35396  satfv1fvfmla1  35406  altopthg  35951  altopthbg  35952  brsegle  36092  bj-imdirvallem  37164  finxpreclem3  37377  itg2addnclem3  37663  exan3  38278  exanres  38279  exanres3  38280  eqrel2  38283  brcoss  38418  brcoss3  38420  brcoels  38422  br1cossxrnres  38435  brcosscnv  38459  prtlem13  38857  dib1dim  41154  f1o2d2  42216  pellex  42818  tfsconcatb0  43327  tfsconcat00  43330  prsprel  47481  uspgrsprf1  48141  uspgrsprfo  48142  brab2ddw2  48824