Theorem anbi1i 446

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 443	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))

Syntax hints:   ∧ wa 102   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anbi2ci  447  anbi12i  448  an12  526  anandi  555  pm5.53  749  pm5.75  904  3ancoma  927  3ioran  935  an6  1253  19.26-3an  1413  19.28h  1495  19.28  1496  eeeanv  1851  sb3an  1875  moanim  2017  nfrexdya  2407  r19.26-3  2493  r19.41  2515  rexcomf  2522  3reeanv  2530  cbvreu  2581  ceqsex3v  2651  rexab  2764  rexrab  2765  rmo4  2795  reuind  2805  sbc3an  2885  rmo3  2915  ssrab  3082  rexun  3163  elin3  3174  inass  3193  unssdif  3216  indifdir  3237  difin2  3243  inrab2  3254  rabun2  3260  reuun2  3264  undif4  3323  rexsns  3451  rexdifsn  3541  2ralunsn  3611  iuncom4  3706  iunxiun  3778  inuni  3951  unidif0  3962  bnd2  3968  otth2  4025  copsexg  4028  copsex4g  4031  opeqsn  4036  opelopabsbALT  4043  suc11g  4329  rabxp  4427  opeliunxp  4442  xpundir  4444  xpiundi  4445  xpiundir  4446  brinxp2  4454  rexiunxp  4527  brres  4667  brresg  4669  dmres  4681  resiexg  4704  dminss  4789  imainss  4790  ssrnres  4814  elxp4  4859  elxp5  4860  cnvresima  4861  coundi  4873  resco  4876  imaco  4877  coiun  4881  coi1  4887  coass  4890  xpcom  4915  dffun2  4963  fncnv  5017  imadiflem  5030  imadif  5031  imainlem  5032  mptun  5081  fcnvres  5125  dff1o2  5184  dff1o3  5185  ffoss  5211  f11o  5212  brprcneu  5224  fvun2  5294  eqfnfv3  5321  respreima  5349  f1ompt  5374  fsn  5389  abrexco  5452  imaiun  5453  f1mpt  5464  dff1o6  5469  oprabid  5590  dfoprab2  5605  oprab4  5628  mpt2mptx  5648  opabex3d  5801  opabex3  5802  abexssex  5805  dfopab2  5868  dfoprab3s  5869  1stconst  5895  2ndconst  5896  xporderlem  5905  spc2ed  5907  f1od2  5909  brtpos2  5922  tpostpos  5935  tposmpt2  5952  oviec  6301  domen  6321  xpsnen  6388  xpcomco  6393  xpassen  6397  ltexpi  6666  dfmq0qs  6758  dfplq0qs  6759  enq0enq  6760  enq0ref  6762  enq0tr  6763  nqnq0pi  6767  prnmaxl  6817  prnminu  6818  addsrpr  7061  mulsrpr  7062  addcnsr  7141  mulcnsr  7142  ltresr  7146  addvalex  7151  axprecex  7185  elnnz  8519  fnn0ind  8621  rexuz2  8827  qreccl  8885  rexrp  8914  elixx3g  9077  elfz2  9189  elfzuzb  9192  fznn  9259  elfz2nn0  9282  fznn0  9283  4fvwrd4  9304  elfzo2  9314  fzind2  9402  cvg1nlemres  10097  divalgb  10557  bezoutlemmain  10619  isprm2  10731  oddpwdc  10784  bdcriota  10966  bj-peano4  11042  alsconv  11083