Theorem anbi2i 445

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 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:  anbi12i  448  mpan10  458  an4  553  an42  554  anandir  558  dcim  822  19.27h  1497  19.27  1498  19.41  1621  sbcof2  1738  sbidm  1779  sb6  1814  3exdistr  1840  4exdistr  1841  2sb5  1907  2sb5rf  1913  sbel2x  1922  eu2  1992  euan  2004  sbmo  2007  mo4f  2008  eu4  2010  moanim  2022  2eu4  2041  clelab  2212  nonconne  2267  r2exf  2396  ceqsex3v  2661  ceqsex4v  2662  ceqsex8v  2664  reu2  2801  reu6  2802  reu4  2807  reu7  2808  rmo3f  2810  rmo4f  2811  2rmorex  2819  rmo3  2928  raldifb  3138  inass  3208  dfss4st  3230  ssddif  3231  difin  3234  invdif  3239  indif  3240  indi  3244  difundi  3249  difindiss  3251  inssdif0im  3347  ssdifsn  3563  unipr  3662  uniun  3667  uniin  3668  iunin2  3788  iindif2m  3792  iinin2m  3793  unidif0  3994  mss  4044  eqvinop  4061  opcom  4068  opeqsn  4070  uniuni  4264  zfinf2  4394  elnn  4410  fconstmpt  4473  opeliunxp  4481  xpundi  4482  elvvv  4489  xpiindim  4561  elcnv2  4602  cnvuni  4610  dmuni  4634  opelres  4706  elima3  4768  imai  4775  imainss  4834  ssrnres  4860  cnvresima  4907  mptpreima  4911  coundir  4920  rnco  4924  coass  4936  relrelss  4944  dffun2  5012  dffun4  5013  dffun6f  5015  dffun4f  5018  dffun7  5028  dffun8  5029  dffun9  5030  svrelfun  5065  fncnv  5066  funcnvuni  5069  dfmpt3  5122  fintm  5180  fin  5181  dff12  5199  fores  5226  dff1o4  5245  eqfnfv3  5383  unpreima  5408  ffnfvf  5441  dff13f  5531  ffnov  5731  eqfnov  5733  foov  5773  opabex3d  5874  opabex3  5875  mpt2xopovel  5988  tpostpos  6011  dfsmo2  6034  tfr1onlemaccex  6095  tfrcllembxssdm  6103  tfrcllemaccex  6108  tfrcllemres  6109  tfrcldm  6110  erinxp  6346  mapsncnv  6432  mapsnen  6508  xpassen  6526  distrnqg  6925  subhalfnqq  6952  enq0enq  6969  enq0sym  6970  enq0tr  6972  addnq0mo  6985  mulnq0mo  6986  distrnq0  6997  prarloc  7041  nqprrnd  7081  ltexprlemopl  7139  ltexprlemlol  7140  ltexprlemopu  7141  ltexprlemupu  7142  ltexprlemdisj  7144  ltexprlemloc  7145  recexprlemdisj  7168  caucvgprprlemell  7223  caucvgprprlemelu  7224  addsrmo  7268  mulsrmo  7269  opelreal  7344  axcaucvglemres  7413  elnnz  8730  elznn0nn  8734  zltlen  8795  suprzclex  8814  peano2uz2  8823  peano5uzti  8824  qltlen  9094  elfzuzb  9403  4fvwrd4  9516  fzind2  9615  cvg1nlemres  10383  rexfiuz  10387  cbvsum  10713  ndvdssub  11023  isprm2  11192  isprm4  11194  hashdvds  11290