Theorem anbi2i 480

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

Hypothesis

Ref	Expression
bi.aa	|- (ph <-> ps)

Assertion

Ref	Expression
anbi2i	|- ((ch /\ ph) <-> (ch /\ ps))

Proof of Theorem anbi2i

Step	Hyp	Ref	Expression
1		bi.aa	. . . 4 |- (ph <-> ps)
2	1	biimp 151	. . 3 |- (ph -> ps)
3	2	anim2i 335	. 2 |- ((ch /\ ph) -> (ch /\ ps))
4	1	biimpr 152	. . 3 |- (ps -> ph)
5	4	anim2i 335	. 2 |- ((ch /\ ps) -> (ch /\ ph))
6	3, 5	impbi 157	1 |- ((ch /\ ph) <-> (ch /\ ps))

Syntax hints:   <-> wb 146   /\ wa 223

This theorem is referenced by:  anbi1i 481  anbi12i 482  an23 485  an4 506  an42 507  anandir 511  3imtr3g 552  oranabs 582  bibi2i 608  xor2 673  rnlem 773  19.27 1069  sb6 1267  3exdistr 1312  4exdistr 1313  eeeanv 1324  2sb5 1335  2sb5rf 1338  sbel2x 1345  eu2 1396  eu3 1397  mo4f 1402  eu5 1409  eu4 1410  euan 1428  2mos 1448  2eu4 1452  2eu6 1454  clelab 1581  r2ex 1691  reu2 1930  reu3 1931  reu4 1934  reu7 1935  dfpss2 2133  dfpss3 2134  difdif 2166  inass 2223  dfss4 2242  dfin2 2244  difin 2245  indi 2251  difin0ss 2332  inssdif0 2333  eluniab 2513  unipr 2515  uniun 2519  uniin 2520  dfiun2g 2586  iunin2 2608  iundif2 2610  iindif2 2611  axrep1 2694  axrep4 2697  notzfaus 2741  eqvinop 2791  opeqsn 2802  opabid 2810  uniuni 2880  ordtri3or 2979  onzsl 3117  findsg 3157  tfindsg 3162  fconstopab 3210  xpundi 3225  elcnv2 3294  cnvuni 3301  dmuni 3319  opelres 3372  dfima3 3406  elima3 3410  imai 3417  asymref2 3440  intirr 3441  rnuni 3459  imainss 3463  ssrnres 3481  rninxp 3482  cores 3499  rnco 3502  coass 3512  dffun2 3526  dffun3 3527  dffun4 3528  dffun5 3529  dffunmof 3530  funeu2 3538  dffun6 3539  dffun8 3541  svrelfun 3560  fncnv 3561  funcnvuni 3564  imadif 3574  fcoi2 3646  fconst 3658  f11 3664  fores 3681  f1o4 3696  f1o5 3697  f1ocnv 3701  fvopab2 3791  eqfnfvf 3798  ffnfvf 3829  fsn2 3836  funiunfv 3866  f1fvf 3875  tfrlem2 3912  dfrdg2 3933  rdglem1 3937  tz7.49 3959  ffnoprval 4014  eqfnoprval 4016  fooprval 4037  2ndconst 4097  foprab2 4119  th3qlem1 4314  mapsnen 4429  xpassen 4441  pw2en 4446  xpmapenlem5 4500  abfii1OLD 4561  abfii2OLD 4562  inf2 4608  axinf 4623  trcl 4645  aceq1 4729  aceq3 4733  aceq4 4734  aceq5lem2 4736  aceq5lem3 4737  aceq5 4740  kmlem3 4767  kmlem4 4768  kmlem14 4778  kmlem15 4779  aceqkm 4781  zorn2lem7 4794  brdom7disj 4804  brdom6disj 4805  cf0 4910  zfcndrep 4966  zfcndinf 4970  distrlem1pr 5127  distrlem5pr 5131  opelreal 5249  elreal 5250  pre-axsup 5291  elnnz 6145  elznn0nn 6148  peano2uz2 6201  nnwof 6459  nnwos 6460  elfzuzb 6476  cau3ir 6915  cbvsum 6986  clm1 7077  climcmplem 7137  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  cvgratlem3 7252  elcncf1d 7270  infpn2 7509  infmap2lem1 7579  infmap2 7581  istop2gOLD 7597  istps4OLD 7609  isbasis2g 7612  tgval2t 7617  tgval3t 7625  tgss3t 7638  basgent 7640  subtop 7646  fctop2 7651  clsval2 7685  cncnp 7778  blfval2 7836  blf 7844  iscau2 7937  xpcn 7976  oprcn 7977  fsumcnlem 7989  bcthlem4 8002  bcthlem12 8010  bcthlem14 8012  bcthlem32 8030  sspval 8382  ubthlem1 8529  spwval2 8653  spwmo 8656  pilem1 8671  axgroth4 8780  grothprim 8783  hlimcaui 9106  ocsh 9156  pjtheu 9235  shscl 9281  h1deot 9472  h1det 9473  hommvalt 9512  hfmmvalt 9515  nmcopexlem1 9951  nmcopexlem2 9952  nmcfnexlem1 9980  nmcfnexlem2 9981  pjhmopidm 10110  cvbr2t 10210  cvnbtwn2t 10214  cvnbtwn4t 10216  mdsl2 10249  cvmd 10251  mdsymlem6 10335  cdj3lem3b 10367  ahypfmbi 10426  eeeeanv 10436  infiOLD 10579  ishgrag 10769

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain