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 551  oranabs 581  bibi2i 607  xor2 672  rnlem 772  19.27 1067  sb6 1265  3exdistr 1310  4exdistr 1311  eeeanv 1322  2sb5 1333  2sb5rf 1336  sbel2x 1343  eu2 1394  eu3 1395  mo4f 1400  eu5 1407  eu4 1408  euan 1426  2mos 1446  2eu4 1450  2eu6 1452  clelab 1578  r2ex 1688  reu2 1926  reu3 1927  reu4 1930  reu7 1931  dfpss2 2129  dfpss3 2130  difdif 2162  inass 2219  dfss4 2238  dfin2 2240  difin 2241  indi 2247  difin0ss 2328  inssdif0 2329  eluniab 2508  unipr 2510  uniun 2514  uniin 2515  dfiun2g 2581  iunin2 2603  iundif2 2605  iindif2 2606  axrep1 2689  axrep4 2692  notzfaus 2736  eqvinop 2786  opeqsn 2797  opabid 2805  uniuni 2875  ordtri3or 2974  onzsl 3112  findsg 3152  tfindsg 3157  fconstopab 3205  xpundi 3220  elcnv2 3289  cnvuni 3296  dmuni 3314  opelres 3364  dfima3 3398  elima3 3402  imai 3409  asymref2 3432  intirr 3433  rnuni 3451  imainss 3455  ssrnres 3473  rninxp 3474  cores 3491  rnco 3494  coass 3504  dffun2 3518  dffun3 3519  dffun4 3520  dffun5 3521  dffunmof 3522  funeu2 3530  dffun6 3531  dffun8 3533  svrelfun 3552  fncnv 3553  funcnvuni 3556  imadif 3566  fcoi2 3637  fconst 3649  f11 3655  fores 3672  f1o4 3687  f1o5 3688  f1ocnv 3692  fvopab2 3782  eqfnfvf 3789  ffnfvf 3820  fsn2 3827  funiunfv 3857  f1fvf 3866  tfrlem2 3903  dfrdg2 3924  rdglem1 3928  tz7.49 3950  ffnoprval 4005  eqfnoprval 4007  fooprval 4028  2ndconst 4087  foprab2 4109  th3qlem1 4304  mapsnen 4416  xpassen 4427  pw2en 4432  xpmapenlem5 4486  abfii1 4541  abfii2 4542  inf2 4588  axinf 4603  trcl 4625  aceq1 4709  aceq3 4713  aceq4 4714  aceq5lem2 4716  aceq5lem3 4717  aceq5 4720  kmlem3 4747  kmlem4 4748  kmlem14 4758  kmlem15 4759  aceqkm 4761  zorn2lem7 4774  brdom7disj 4784  brdom6disj 4785  cf0 4890  zfcndrep 4946  zfcndinf 4950  distrlem1pr 5107  distrlem5pr 5111  opelreal 5229  elreal 5230  pre-axsup 5271  elnnz 6100  elznn0nn 6103  peano2uz2 6157  nnwof 6399  nnwos 6400  elfzuzb 6416  cau3ir 6860  cbvsum 6932  clm1 7023  climcmplem 7081  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  cvgratlem3 7195  elcncf1d 7213  ivth2OLD 7242  infpn2 7460  infmap2lem1 7529  infmap2 7531  istop2g 7547  istps4 7559  isbasis2g 7562  tgval2t 7567  tgval3t 7575  tgss3t 7588  basgent 7590  subtop 7596  fctop2 7601  clsval2 7635  cncnp 7728  blfval2 7788  blf 7796  iscau2 7889  xpcn 7926  oprcn 7927  fsumcnlem 7939  bcthlem4 7952  bcthlem12 7960  bcthlem14 7962  bcthlem32 7980  sspval 8329  ubthlem1 8473  spwval2 8595  spwmo 8598  pilem1 8609  axgroth4 8719  grothprim 8722  hlimcaui 9045  ocsh 9095  pjtheu 9173  shscl 9219  h1deot 9410  h1det 9411  hommvalt 9452  hfmmvalt 9455  nmcopexlem1 9889  nmcopexlem2 9890  nmcfnexlem1 9918  nmcfnexlem2 9919  pjhmopidm 10048  cvbr2t 10148  cvnbtwn2t 10152  cvnbtwn4t 10154  mdsl2 10186  cvmd 10188  mdsymlem6 10272  cdj3lem3b 10301  ahypfmbi 10362  eeeeanv 10372  infi 10484  ishgrag 10641

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