Theorem anbi1i 458

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

Syntax hints:   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anbi2ci  459  anbi12i  460  bianassc  470  an12  561  anandi  590  pm5.53  804  pm5.75  965  3ancoma  988  3ioran  996  an6  1334  19.26-3an  1507  19.28h  1586  19.28  1587  eeeanv  1962  sb3an  1987  moanim  2129  nfrexdya  2543  r19.26-3  2637  r19.41  2662  rexcomf  2669  3reeanv  2678  cbvreu  2737  ceqsex3v  2817  rexab  2939  rexrab  2940  rmo4  2970  rmo3f  2974  reuind  2982  sbc3an  3064  rmo3  3094  ssrab  3275  rexun  3357  elin3  3368  inass  3387  unssdif  3412  indifdir  3433  difin2  3439  inrab2  3450  rabun2  3456  reuun2  3460  undif4  3527  rexdifpr  3666  rexsns  3677  rexdifsn  3771  2ralunsn  3845  iuncom4  3940  iunxiun  4015  inuni  4207  unidif0  4219  bnd2  4225  otth2  4293  copsexg  4296  copsex4g  4299  opeqsn  4305  opelopabsbALT  4313  elpwpwel  4530  suc11g  4613  rabxp  4720  opeliunxp  4738  xpundir  4740  xpiundi  4741  xpiundir  4742  brinxp2  4750  rexiunxp  4828  brres  4974  brresg  4976  dmres  4989  resiexg  5013  dminss  5106  imainss  5107  ssrnres  5134  elxp4  5179  elxp5  5180  cnvresima  5181  coundi  5193  resco  5196  imaco  5197  coiun  5201  coi1  5207  coass  5210  xpcom  5238  dffun2  5290  fncnv  5349  imadiflem  5362  imadif  5363  imainlem  5364  mptun  5417  fcnvres  5471  dff1o2  5539  dff1o3  5540  ffoss  5566  f11o  5567  brprcneu  5582  fvun2  5659  eqfnfv3  5692  respreima  5721  f1ompt  5744  fsn  5765  abrexco  5841  imaiun  5842  f1mpt  5853  dff1o6  5858  oprabid  5989  dfoprab2  6005  oprab4  6029  mpomptx  6049  opabex3d  6219  opabex3  6220  abexssex  6223  dfopab2  6288  dfoprab3s  6289  1stconst  6320  2ndconst  6321  xporderlem  6330  spc2ed  6332  f1od2  6334  brtpos2  6350  tpostpos  6363  tposmpo  6380  oviec  6741  mapsncnv  6795  dfixp  6800  domen  6853  mapsnen  6917  xpsnen  6931  xpcomco  6936  xpassen  6940  ltexpi  7470  dfmq0qs  7562  dfplq0qs  7563  enq0enq  7564  enq0ref  7566  enq0tr  7567  nqnq0pi  7571  prnmaxl  7621  prnminu  7622  suplocexprlemloc  7854  addsrpr  7878  mulsrpr  7879  suplocsrlemb  7939  addcnsr  7967  mulcnsr  7968  ltresr  7972  addvalex  7977  axprecex  8013  elnnz  9402  fnn0ind  9509  rexuz2  9722  qreccl  9783  rexrp  9818  elixx3g  10043  elfz2  10157  elfzuzb  10161  fznn  10231  elfz2nn0  10254  fznn0  10255  4fvwrd4  10282  elfzo2  10292  fzind2  10390  cvg1nlemres  11371  fsum2dlemstep  11820  modfsummod  11844  fprodseq  11969  divalgb  12311  bezoutlemmain  12394  isprm2  12514  oddpwdc  12571  prdsex  13176  prdsval  13180  prdsbaslemss  13181  xpscf  13254  issubg3  13603  releqgg  13631  eqgex  13632  imasabl  13747  dfrhm2  13991  ntreq0  14679  cnnei  14779  txlm  14826  blres  14981  isms2  15001  dedekindicclemicc  15179  limcrcl  15205  lgsquadlem1  15629  lgsquadlem2  15630  bdcriota  15957  bj-peano4  16029  alsconv  16160