Theorem anbi1i 462

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

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi2ci  463  anbi12i  464  bianassc  474  an12  567  anandi  598  pm5.53  814  pm5.75  975  3ancoma  1016  3ioran  1024  an6  1362  19.26-3an  1536  19.28h  1615  19.28  1616  eeeanv  1993  sb3an  2018  moanim  2161  nfrexdya  2586  r19.26-3  2681  r19.41  2706  rexcomf  2713  3reeanv  2722  cbvreu  2784  ceqsex3v  2865  rexab  2988  rexrab  2989  rmo4  3019  rmo3f  3023  reuind  3031  sbc3an  3113  rmo3  3144  ssrab  3326  rexun  3409  elin3  3420  inass  3441  unssdif  3466  indifdir  3487  difin2  3493  inrab2  3506  rabun2  3512  reuun2  3516  undif4  3587  rexdifpr  3737  rexsns  3748  rexdifsn  3846  2ralunsn  3924  iuncom4  4019  iunxiun  4094  inuni  4291  unidif0  4304  bnd2  4310  otth2  4381  copsexg  4384  copsex4g  4387  opeqsn  4393  opelopabsbALT  4401  elpwpwel  4621  suc11g  4704  rabxp  4812  opeliunxp  4830  xpundir  4832  xpiundi  4833  xpiundir  4834  brinxp2  4842  rexiunxp  4922  brres  5069  brresg  5071  dmres  5084  resiexg  5108  dminss  5202  imainss  5203  ssrnres  5230  elxp4  5275  elxp5  5276  cnvresima  5277  coundi  5289  resco  5292  imaco  5293  coiun  5297  coi1  5303  coass  5306  xpcom  5334  dffun2  5387  fncnv  5447  imadiflem  5460  imadif  5461  imainlem  5462  mptun  5515  fcnvres  5575  dff1o2  5644  dff1o3  5645  ffoss  5672  f11o  5673  brprcneu  5688  fvun2  5770  eqfnfv3  5808  respreima  5836  f1ompt  5859  fsn  5880  abrexco  5965  imaiun  5966  f1mpt  5977  dff1o6  5982  oprabid  6117  dfoprab2  6135  oprab4  6159  mpomptx  6179  opabex3d  6350  opabex3  6351  abexssex  6354  dfopab2  6423  dfoprab3s  6424  1stconst  6457  2ndconst  6458  xporderlem  6467  spc2ed  6469  f1od2  6471  brtpos2  6522  tpostpos  6535  tposmpo  6552  oviec  6915  mapsncnv  6977  dfixp  6982  domen  7035  mapsnen  7100  xpsnen  7119  xpcomco  7124  xpassen  7128  sspw1or2  7545  ltexpi  7705  dfmq0qs  7797  dfplq0qs  7798  enq0enq  7799  enq0ref  7801  enq0tr  7802  nqnq0pi  7806  prnmaxl  7856  prnminu  7857  suplocexprlemloc  8089  addsrpr  8113  mulsrpr  8114  suplocsrlemb  8174  addcnsr  8202  mulcnsr  8203  ltresr  8207  addvalex  8212  axprecex  8248  elnnz  9659  fnn0ind  9767  rexuz2  9991  qreccl  10052  rexrp  10088  elixx3g  10314  elfz2  10429  elfzuzb  10433  fznn  10507  elfz2nn0  10530  fznn0  10531  4fvwrd4  10558  elfzo2  10568  fzind2  10669  sseqn  11295  hashf1lem1  11301  hashf1lem2  11302  cvg1nlemres  11767  fsum2dlemstep  12220  modfsummod  12244  fprodseq  12369  divalgb  12711  bezoutlemmain  12794  isprm2  12914  nnmaxpw  12972  ballotfilemelo  13274  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  xpscf  13721  issubg3  14048  releqgg  14076  eqgex  14077  imasabl  14224  prdsex  14256  prdsval  14257  prdsbaslemss  14258  dfrhm2  14545  drngprop  14701  isassa  15086  ntreq0  15324  cnnei  15424  txlm  15471  blres  15626  isms2  15646  dedekindicclemicc  15824  limcrcl  15850  lgsquadlem1  16362  lgsquadlem2  16363  isclwwlknx  16823  clwwlknonel  16839  clwwlknon2x  16842  iseupthf1o  16855  bdcriota  17075  bj-peano4  17147  alsanmo  17318  ralsanmo  17319  alsralrex  17320  alsraln0m  17321