Theorem bi2anan9 649

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  bi2anan9r  650  rspc2gv  3591  2reu5  3721  ralprgf  4660  ralprg  4662  raltpg  4664  prssg  4785  prsspwg  4789  ssprss  4790  intprg  4946  opelopab2a  5519  brab2d  5522  opelxp  5697  eqrel  5770  eqrelrel  5783  brcog  5852  tpres  7199  dff13  7252  cbvmpov  7505  resoprab2  7529  ovig  7556  dfoprab4f  8049  f1o2ndf1  8113  mpof1o2d  8117  om00el  8557  oeoe  8581  eroveu  8806  endisj  9048  infxpen  10003  sornom  10265  ltsrpr  11066  axcnre  11153  axmulgt0  11288  wloglei  11750  mulge0b  12089  addltmul  12484  ltxr  13144  fzadd2  13592  sumsqeq0  14220  ccat0  14618  rlim  15551  cpnnen  16289  dvds2lem  16330  opoe  16425  omoe  16426  opeo  16427  omeo  16428  gcddvds  16565  dfgcd2  16608  pcqmul  16917  xpsfrnel2  17622  eqgval  19249  frgpuplem  19846  mpfind  22275  2ndcctbss  23621  txbasval  23772  cnmpt12  23833  cnmpt22  23840  prdsxmslem2  24695  ishtpy  25140  bcthlem1  25492  bcth  25497  volun  25713  vitali  25781  itg1addlem3  25866  rolle  26158  mumullem2  27353  lgsquadlem3  27555  lgsquad  27556  2sqlem7  27597  cutsval  27982  lesrec  28001  remulscllem2  28703  elplngid  29073  lnincplng  29075  plngcp  29077  plngrot  29081  nhpmirhp  29089  lnperpexs  29123  ragraghl  29158  brprlng  29197  prlnghpg  29205  prlngmo  29213  axpasch  29300  wlkson  30013  iswwlksnon  30211  wpthswwlks2on  30322  eulplig  30846  hlimi  31549  leopadd  32493  tpssg  32892  eqrelrd2  32970  cntzun  33408  isinftm  33510  finexttrb  34064  metidv  34291  satfv1  35863  satfbrsuc  35866  gonarlem  35894  satfv0fvfmla0  35913  satfv1fvfmla1  35923  altopthg  36467  altopthbg  36468  brsegle  36608  nmuladdss  36713  bj-imdirvallem  37852  finxpreclem3  38067  itg2addnclem3  38352  exan3  38977  exanres  38978  exanres3  38979  eqrel2  38982  sucmapleftuniq  39167  brcoss  39198  brcoss3  39200  brcoels  39202  br1cossxrnres  39215  brcosscnv  39239  disjimeceqim2  39482  eldisjim3  39492  prtlem13  39670  dib1dim  41967  pellex  43590  tfsconcatb0  44099  tfsconcat00  44102  prsprel  48264  uspgrsprf1  48940  uspgrsprfo  48941  brab2ddw2  49636