Theorem anbi2i 457

Description: Introduce a left 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
anbi2i	⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))

Proof of Theorem anbi2i

Step	Hyp	Ref	Expression
1		bi.aa	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.32i 454	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:  anbi12i  460  bianass  469  mpan10  474  an4  586  an42  587  anandir  591  dcim  842  19.27h  1571  19.27  1572  19.41  1697  sbcof2  1821  sbidm  1862  sb6  1898  3exdistr  1927  4exdistr  1928  2sb5  1995  2sb5rf  2001  sbel2x  2010  eu2  2082  euan  2094  sbmo  2097  mo4f  2098  eu4  2100  moanim  2112  2eu4  2131  clelab  2315  nonconne  2372  r2exf  2508  ceqsex3v  2794  ceqsex4v  2795  ceqsex8v  2797  reu2  2940  reu6  2941  reu4  2946  reu7  2947  rmo3f  2949  rmo4f  2950  2rmorex  2958  rmo3  3069  raldifb  3290  inass  3360  dfss4st  3383  ssddif  3384  difin  3387  invdif  3392  indif  3393  indi  3397  difundi  3402  difindiss  3404  inssdif0im  3505  rexdifpr  3635  ssdifsn  3735  unipr  3838  uniun  3843  uniin  3844  iunin2  3965  iindif2m  3969  iinin2m  3970  elpwpw  3988  unidif0  4185  mss  4244  eqvinop  4261  opcom  4268  opeqsn  4270  uniuni  4469  zfinf2  4606  elomssom  4622  fconstmpt  4691  opeliunxp  4699  xpundi  4700  elvvv  4707  xpiindim  4782  elcnv2  4823  cnvuni  4831  dmuni  4855  opelres  4930  restidsing  4981  elima3  4995  imai  5002  imainss  5062  ssrnres  5089  cnvresima  5136  mptpreima  5140  coundir  5149  rnco  5153  coass  5165  relrelss  5173  dffun2  5245  dffun4  5246  dffun6f  5248  dffun4f  5251  dffun7  5262  dffun8  5263  dffun9  5264  svrelfun  5300  fncnv  5301  funcnvuni  5304  dfmpt3  5357  fintm  5420  fin  5421  dff12  5439  fores  5466  dff1o4  5488  eqfnfv3  5635  unpreima  5661  ffnfvf  5695  dff13f  5791  ffnov  5999  eqfnov  6002  foov  6042  opabex3d  6145  opabex3  6146  mpoxopovel  6265  tpostpos  6288  dfsmo2  6311  tfr1onlemaccex  6372  tfrcllembxssdm  6380  tfrcllemaccex  6385  tfrcllemres  6386  tfrcldm  6387  erinxp  6634  mapsncnv  6720  cbvixp  6740  ixpin  6748  ixpiinm  6749  mptelixpg  6759  elixpsn  6760  ixpsnf1o  6761  mapsnen  6836  xpassen  6855  2omotaplemap  7285  distrnqg  7415  subhalfnqq  7442  enq0enq  7459  enq0sym  7460  enq0tr  7462  addnq0mo  7475  mulnq0mo  7476  distrnq0  7487  prarloc  7531  nqprrnd  7571  ltexprlemopl  7629  ltexprlemlol  7630  ltexprlemopu  7631  ltexprlemupu  7632  ltexprlemdisj  7634  ltexprlemloc  7635  recexprlemdisj  7658  caucvgprprlemell  7713  caucvgprprlemelu  7714  addsrmo  7771  mulsrmo  7772  opelreal  7855  axcaucvglemres  7927  axpre-suploc  7930  elnnz  9292  elznn0nn  9296  zltlen  9360  suprzclex  9380  peano2uz2  9389  peano5uzti  9390  qltlen  9669  elfzuzb  10048  4fvwrd4  10169  fzind2  10268  cvg1nlemres  11025  rexfiuz  11029  cbvsum  11399  mertenslem2  11575  mertensabs  11576  cbvprod  11597  prodmodc  11617  fprodseq  11622  ndvdssub  11966  nnwosdc  12071  isprm2  12148  isprm4  12150  hashdvds  12252  xpscf  12820  isnsg2  13139  isnsg4  13148  isrhm  13505  issubrng  13543  subsubrng2  13559  subsubrg2  13590  isbasis2g  13997  tgval2  14003  elcncf1di  14518  dedekindicclemicc  14562  dedekindicc  14563