Theorem anbi1i 445

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 442	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  446  anbi12i  447  an12  525  anandi  554  pm5.53  748  pm5.75  903  3ancoma  926  3ioran  934  an6  1252  19.26-3an  1412  19.28h  1494  19.28  1495  eeeanv  1849  sb3an  1873  moanim  2015  nfrexdya  2401  r19.26-3  2487  r19.41  2509  rexcomf  2516  3reeanv  2524  cbvreu  2575  ceqsex3v  2641  rexab  2754  rexrab  2755  rmo4  2785  reuind  2795  sbc3an  2875  rmo3  2905  ssrab  3072  rexun  3152  elin3  3157  inass  3176  unssdif  3199  indifdir  3220  difin2  3226  inrab2  3237  rabun2  3243  reuun2  3247  undif4  3306  rexsns  3432  rexdifsn  3521  2ralunsn  3590  iuncom4  3685  iunxiun  3757  inuni  3930  unidif0  3941  bnd2  3947  otth2  3996  copsexg  3999  copsex4g  4002  opeqsn  4007  opelopabsbALT  4014  suc11g  4300  rabxp  4398  opeliunxp  4413  xpundir  4415  xpiundi  4416  xpiundir  4417  brinxp2  4425  rexiunxp  4496  brres  4636  brresg  4638  dmres  4650  resiexg  4673  dminss  4758  imainss  4759  ssrnres  4783  elxp4  4828  elxp5  4829  cnvresima  4830  coundi  4842  resco  4845  imaco  4846  coiun  4850  coi1  4856  coass  4859  xpcom  4884  dffun2  4932  fncnv  4985  imadiflem  4998  imadif  4999  imainlem  5000  mptun  5049  fcnvres  5093  dff1o2  5151  dff1o3  5152  ffoss  5178  f11o  5179  brprcneu  5191  fvun2  5261  eqfnfv3  5288  respreima  5316  f1ompt  5341  fsn  5356  abrexco  5419  imaiun  5420  f1mpt  5431  dff1o6  5436  oprabid  5557  dfoprab2  5572  oprab4  5595  mpt2mptx  5615  opabex3d  5768  opabex3  5769  abexssex  5772  dfopab2  5835  dfoprab3s  5836  1stconst  5862  2ndconst  5863  xporderlem  5872  spc2ed  5874  f1od2  5876  brtpos2  5889  tpostpos  5902  tposmpt2  5919  oviec  6235  domen  6255  xpsnen  6318  xpcomco  6323  xpassen  6327  ltexpi  6527  dfmq0qs  6619  dfplq0qs  6620  enq0enq  6621  enq0ref  6623  enq0tr  6624  nqnq0pi  6628  prnmaxl  6678  prnminu  6679  addsrpr  6922  mulsrpr  6923  addcnsr  7002  mulcnsr  7003  ltresr  7007  addvalex  7012  axprecex  7046  elnnz  8361  fnn0ind  8463  rexuz2  8669  qreccl  8727  rexrp  8756  elixx3g  8924  elfz2  9036  elfzuzb  9039  fznn  9106  elfz2nn0  9128  fznn0  9129  4fvwrd4  9150  elfzo2  9160  fzind2  9248  cvg1nlemres  9871  divalgb  10325  bezoutlemmain  10387  isprm2  10499  oddpwdc  10552  bdcriota  10674  bj-peano4  10750  alsconv  10791