Theorem anbi2i 430

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

Syntax hints:   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  anbi12i  433  mpan10  443  an4  520  an42  521  anandir  525  dcim  784  19.27h  1452  19.27  1453  19.41  1576  sbcof2  1691  sbidm  1731  sb6  1766  3exdistr  1792  4exdistr  1793  2sb5  1859  2sb5rf  1865  sbel2x  1874  eu2  1944  euan  1956  sbmo  1959  mo4f  1960  eu4  1962  moanim  1974  2eu4  1993  clelab  2162  nonconne  2217  r2exf  2342  ceqsex3v  2596  ceqsex4v  2597  ceqsex8v  2599  reu2  2729  reu6  2730  reu4  2735  reu7  2736  2rmorex  2745  rmo3  2849  dfpss2  3029  raldifb  3083  inass  3147  ssddif  3171  difin  3174  invdif  3179  indif  3180  indi  3184  difundi  3189  difindiss  3191  inssdif0im  3291  unipr  3594  uniun  3599  uniin  3600  iunin2  3720  iindif2m  3724  iinin2m  3725  unidif0  3920  mss  3962  eqvinop  3980  opcom  3987  opeqsn  3989  uniuni  4183  zfinf2  4312  elnn  4328  fconstmpt  4387  opeliunxp  4395  xpundi  4396  elvvv  4403  xpiindim  4473  elcnv2  4513  cnvuni  4521  dmuni  4545  opelres  4617  elima3  4675  imai  4681  imainss  4739  ssrnres  4763  cnvresima  4810  mptpreima  4814  coundir  4823  rnco  4827  coass  4839  relrelss  4844  dffun2  4912  dffun4  4913  dffun6f  4915  dffun4f  4918  dffun7  4928  dffun8  4929  dffun9  4930  svrelfun  4964  fncnv  4965  funcnvuni  4968  dfmpt3  5021  fintm  5075  fin  5076  dff12  5091  fores  5115  dff1o4  5134  eqfnfv3  5267  unpreima  5292  ffnfvf  5324  dff13f  5409  ffnov  5605  eqfnov  5607  foov  5647  opabex3d  5748  opabex3  5749  mpt2xopovel  5856  tpostpos  5879  dfsmo2  5902  erinxp  6180  xpassen  6304  distrnqg  6485  subhalfnqq  6512  enq0enq  6529  enq0sym  6530  enq0tr  6532  addnq0mo  6545  mulnq0mo  6546  distrnq0  6557  prarloc  6601  nqprrnd  6641  ltexprlemopl  6699  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  ltexprlemdisj  6704  ltexprlemloc  6705  recexprlemdisj  6728  caucvgprprlemell  6783  caucvgprprlemelu  6784  addsrmo  6828  mulsrmo  6829  opelreal  6904  axcaucvglemres  6973  elnnz  8255  elznn0nn  8259  zltlen  8319  peano2uz2  8345  peano5uzti  8346  qltlen  8575  elfzuzb  8884  4fvwrd4  8997  fzind2  9095  cvg1nlemres  9584