Theorem anbi2i 367

Description: Introduce a left conjunct to both sides of a logical equivalence.

Hypothesis

Ref	Expression
bi.aa	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
anbi2i	⊢ ((χ ∧ φ) ↔ (χ ∧ ψ))

Proof of Theorem anbi2i

Step	Hyp	Ref	Expression
1		bi.aa	. . . 4 ⊢ (φ ↔ ψ)
2	1	biimp 133	. . 3 ⊢ (φ → ψ)
3	2	anim2i 270	. 2 ⊢ ((χ ∧ φ) → (χ ∧ ψ))
4	1	biimpr 134	. . 3 ⊢ (ψ → φ)
5	4	anim2i 270	. 2 ⊢ ((χ ∧ ψ) → (χ ∧ φ))
6	3, 5	impbi 139	1 ⊢ ((χ ∧ φ) ↔ (χ ∧ ψ))

Syntax hints:   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  anbi1i 368  anbi12i 369  an23 371  an4 388  an42 389  anandir 393  3imtr3g 425  bibi2i 460  biass 511  rnlem 579  19.27 750  3exdistr 970  4exdistr 971  eeeanv 981  sbel2x 995  eu2 1023  eu3 1024  mo4f 1028  eu5 1035  eu4 1036  euanv 1053  2eu4 1070  axinf 1084  clelab 1187  sbabel 1189  r2ex 1241  reu2 1338  reu4 1340  zfrep2 1475  dfpss2 1557  dfpss3 1558  difdif 1595  inass 1650  dfss4 1667  dfin2 1669  difin 1670  indi 1676  difin0ss 1753  inssdif0 1754  eqvinop 1901  eluniab 1926  unpr 1930  uniun 1934  uniin 1935  dfiun2 2014  iunin2 2030  iundif2 2032  iindif2 2033  opabid 2099  so 2152  ordtri3or 2230  onzsl 2367  fconstopab 2448  xpundi 2461  elcnv2 2515  cnvuni 2521  dmuni 2538  opelres 2579  dfima3 2605  elima3 2608  imai 2613  intirr 2628  rnuni 2646  imainss 2649  cores 2659  coass 2667  dffun2 2674  dffun3 2675  dffun4 2676  dffun5 2677  dffunmof 2678  funeu2 2686  dffun6 2687  funcnvuni 2706  imadif 2714  fcoi2 2766  fconst 2774  f11 2780  fores 2794  f1o4 2807  f1o5 2808  f1ocnv 2811  fvopab2 2878  cleqfvf 2881  fsn2 2896  f1fvf 2917  tfrlem2 2950  rdglem1 2975  ffnoprval 3041  th3qlem1 3250  mapsnen 3334  xpassen 3344  pw2en 3348  xpmapenlem5 3395  inf0 3457  inf2 3459  trcl 3489  aceq1 3552  aceq3 3556  aceq4 3557  aceq5lem2 3559  aceq5lem3 3560  aceq5 3563  kmlem3 3582  kmlem4 3583  kmlem14 3593  kmlem15 3594  cf0 3705  zfcndrep 3760  zfcndinf 3764  elni 3798  distrlem1pr 3921  distrlem5pr 3925  opelreal 4043  elreal 4044  axsup 4088  elnnz 4572  elznn0nn 4575  peano2uz 4602  nnwof 4609  nnwos 4610  infmap2lem1 4951  infmap2 4953  hlimcaui 5141  ocsh 5164  pjthu 5241  pjthu2 5242  shscl 5282  h1deot 5454  h1det 5455  cvbr2t 5715  cvnbtwn2t 5719  cvnbtwn4t 5721  mdsymlem6 5781

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org