Theorem anbi1i 449

Description: Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
bi.aa	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
anbi1i	⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))

Proof of Theorem anbi1i

Step	Hyp	Ref	Expression
1		bi.aa	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.32ri 446	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi2ci  450  anbi12i  451  an12  531  anandi  560  pm5.53  757  pm5.75  914  3ancoma  937  3ioran  945  an6  1267  19.26-3an  1427  19.28h  1509  19.28  1510  eeeanv  1868  sb3an  1892  moanim  2034  nfrexdya  2429  r19.26-3  2521  r19.41  2544  rexcomf  2551  3reeanv  2559  cbvreu  2610  ceqsex3v  2683  rexab  2799  rexrab  2800  rmo4  2830  rmo3f  2834  reuind  2842  sbc3an  2922  rmo3  2952  ssrab  3122  rexun  3203  elin3  3214  inass  3233  unssdif  3258  indifdir  3279  difin2  3285  inrab2  3296  rabun2  3302  reuun2  3306  undif4  3372  rexsns  3510  rexdifsn  3602  2ralunsn  3672  iuncom4  3767  iunxiun  3840  inuni  4020  unidif0  4031  bnd2  4037  otth2  4101  copsexg  4104  copsex4g  4107  opeqsn  4112  opelopabsbALT  4119  elpwpwel  4334  suc11g  4410  rabxp  4514  opeliunxp  4532  xpundir  4534  xpiundi  4535  xpiundir  4536  brinxp2  4544  rexiunxp  4619  brres  4761  brresg  4763  dmres  4776  resiexg  4800  dminss  4889  imainss  4890  ssrnres  4917  elxp4  4962  elxp5  4963  cnvresima  4964  coundi  4976  resco  4979  imaco  4980  coiun  4984  coi1  4990  coass  4993  xpcom  5021  dffun2  5069  fncnv  5125  imadiflem  5138  imadif  5139  imainlem  5140  mptun  5190  fcnvres  5242  dff1o2  5306  dff1o3  5307  ffoss  5333  f11o  5334  brprcneu  5346  fvun2  5420  eqfnfv3  5452  respreima  5480  f1ompt  5503  fsn  5524  abrexco  5592  imaiun  5593  f1mpt  5604  dff1o6  5609  oprabid  5735  dfoprab2  5750  oprab4  5774  mpomptx  5794  opabex3d  5950  opabex3  5951  abexssex  5954  dfopab2  6017  dfoprab3s  6018  1stconst  6048  2ndconst  6049  xporderlem  6058  spc2ed  6060  f1od2  6062  brtpos2  6078  tpostpos  6091  tposmpo  6108  oviec  6465  mapsncnv  6519  dfixp  6524  domen  6575  mapsnen  6635  xpsnen  6644  xpcomco  6649  xpassen  6653  ltexpi  7046  dfmq0qs  7138  dfplq0qs  7139  enq0enq  7140  enq0ref  7142  enq0tr  7143  nqnq0pi  7147  prnmaxl  7197  prnminu  7198  addsrpr  7441  mulsrpr  7442  addcnsr  7521  mulcnsr  7522  ltresr  7526  addvalex  7531  axprecex  7565  elnnz  8916  fnn0ind  9019  rexuz2  9226  qreccl  9284  rexrp  9313  elixx3g  9525  elfz2  9638  elfzuzb  9641  fznn  9710  elfz2nn0  9733  fznn0  9734  4fvwrd4  9758  elfzo2  9768  fzind2  9857  cvg1nlemres  10597  fsum2dlemstep  11042  modfsummod  11066  divalgb  11417  bezoutlemmain  11479  isprm2  11591  oddpwdc  11644  ntreq0  12083  cnnei  12182  txlm  12229  blres  12362  isms2  12382  limcrcl  12509  bdcriota  12662  bj-peano4  12738  alsconv  12828