Theorem anbi12i 678

Description: Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
anbi12.1	⊢ (φ ↔ ψ)
anbi12.2	⊢ (χ ↔ θ)

Assertion

Ref	Expression
anbi12i	⊢ ((φ ∧ χ) ↔ (ψ ∧ θ))

Proof of Theorem anbi12i

Step	Hyp	Ref	Expression
1		anbi12.1	. . 3 ⊢ (φ ↔ ψ)
2	1	anbi1i 676	. 2 ⊢ ((φ ∧ χ) ↔ (ψ ∧ χ))
3		anbi12.2	. . 3 ⊢ (χ ↔ θ)
4	3	anbi2i 675	. 2 ⊢ ((ψ ∧ χ) ↔ (ψ ∧ θ))
5	2, 4	bitri 240	1 ⊢ ((φ ∧ χ) ↔ (ψ ∧ θ))

Syntax hints:   ↔ wb 176   ∧ wa 358

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  anbi12ci  679  ordi  834  ordir  835  orddi  839  pm5.17  858  xor  861  3anbi123i  1140  an6  1261  nanbi  1294  cadan  1392  nic-axALT  1439  19.43OLD  1606  nfimdOLD  1809  sbbi  2071  sbnf2  2108  eu1  2225  2eu1  2284  2eu4  2287  2eu6  2289  sbabel  2515  neanior  2601  rexeqbii  2645  r19.26m  2749  reean  2777  2ralor  2780  reu5  2824  reu2  3024  reu3  3026  2reu5lem3  3043  eqss  3287  unss  3437  ralunb  3444  ssin  3477  undi  3502  indifdir  3511  undif3  3515  inab  3522  difab  3523  reuss2  3535  reupick  3539  prss  3861  sstp  3870  tpss  3871  prsspw  3878  uniin  3911  intun  3958  intpr  3959  inxpk  4277  sikexlem  4295  dfidk2  4313  ndisjrelk  4323  dfpw2  4327  dfaddc2  4381  dfnnc2  4395  addccom  4406  addcass  4415  nnsucelrlem1  4424  nnsucelrlem2  4425  preaddccan2lem1  4454  ltfinex  4464  ssfin  4470  eqpw1relk  4479  ncfinraiselem2  4480  ncfinraise  4481  ncfinlowerlem1  4482  ncfinlower  4483  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  nnpweq  4523  srelk  4524  sfin112  4529  sfintfinlem1  4531  tfinnnlem1  4533  sfinltfin  4535  spfinex  4537  dfphi2  4569  dfop2lem1  4573  copsex4g  4610  opeqexb  4620  brin  4693  brdif  4694  setconslem1  4731  setconslem2  4732  dfswap2  4741  dfco1  4748  opelxp  4811  elxp3  4831  opbrop  4841  eqrel  4845  eqopr  4847  inopab  4862  inxp  4863  cnvco  4894  dmin  4913  cnvdif  5034  xpnz  5045  xp11  5056  dfco2  5080  dfxp2  5113  dffun4  5121  funun  5146  fun11  5159  fununi  5160  imadif  5171  fnres  5199  fnopabg  5205  fco  5231  fun  5236  fin  5246  f1co  5264  foco  5279  dff1o2  5291  f1oco  5308  tz6.12  5345  fsn  5432  dff1o6  5475  isotr  5495  isomin  5496  dfid4  5503  1stfo  5505  2ndfo  5506  funsi  5520  trtxp  5781  oteltxp  5782  brtxp  5783  dmtxp  5802  txpcofun  5803  fntxp  5804  otsnelsi3  5805  releqmpt  5808  releqmpt2  5809  composeex  5820  disjex  5823  addcfnex  5824  funsex  5828  fnsex  5832  qrpprod  5836  dmpprod  5840  fnpprod  5843  f1opprod  5844  crossex  5850  pw1fnex  5852  pw1fnf1o  5855  fnfullfunlem1  5856  domfnex  5870  ranfnex  5871  clos1ex  5876  dfnnc3  5885  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  ider  5943  ssetpov  5944  eqer  5961  mapexi  6003  mapval2  6018  enex  6031  entr  6038  fundmen  6043  unen  6048  xpen  6055  xpassenlem  6056  xpassen  6057  enpw1lem1  6061  enpw1  6062  enmap2lem4  6066  enmap1lem4  6072  enprmaplem1  6076  enprmaplem4  6079  nenpw1pwlem1  6084  lecex  6115  ovmuc  6130  mucnc  6131  muccl  6132  mucex  6133  muccom  6134  ncdisjeq  6148  tcdi  6164  ovcelem1  6171  ceexlem1  6173  ceex  6174  ce0addcnnul  6179  sbthlem3  6205  sbth  6206  dflec3  6221  nclenc  6222  lenc  6223  tc11  6228  ce2le  6233  tcfnex  6244  muc0or  6252  nnltp1clem1  6261  addccan2nclem2  6264  nmembers1lem1  6268  nncdiv3lem1  6275  nncdiv3lem2  6276  nnc3n3p1  6278  spacvallem1  6281  nchoicelem10  6298  nchoicelem11  6299  nchoicelem16  6304  fnfreclem1  6317