Theorem anbi2i 479

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 480  anbi12i 481  an23 484  an4 505  an42 506  anandir 510  3imtr3g 550  oranabs 580  bibi2i 606  xor2 671  rnlem 771  19.27 1065  sb6 1262  3exdistr 1307  4exdistr 1308  eeeanv 1319  2sb5 1330  2sb5rf 1333  sbel2x 1340  eu2 1389  eu3 1390  mo4f 1395  eu5 1402  eu4 1403  euan 1421  2mos 1441  2eu4 1445  2eu6 1447  clelab 1573  r2ex 1683  reu2 1920  reu3 1921  reu4 1924  reu7 1925  dfpss2 2123  dfpss3 2124  difdif 2156  inass 2213  dfss4 2232  dfin2 2234  difin 2235  indi 2241  difin0ss 2322  inssdif0 2323  eluniab 2503  unipr 2505  uniun 2509  uniin 2510  dfiun2g 2576  iunin2 2598  iundif2 2600  iindif2 2601  axrep1 2684  axrep4 2687  notzfaus 2731  eqvinop 2781  opeqsn 2791  opabid 2799  uniuni 2870  ordtri3or 2969  onzsl 3107  findsg 3147  tfindsg 3152  fconstopab 3200  xpundi 3215  elcnv2 3283  cnvuni 3290  dmuni 3308  opelres 3356  dfima3 3390  elima3 3394  imai 3401  asymref2 3424  asymref2OLD 3426  intirr 3427  rnuni 3445  imainss 3449  ssrnres 3467  rninxp 3468  cores 3485  rnco 3488  coass 3498  dffun2 3512  dffun3 3513  dffun4 3514  dffun5 3515  dffunmof 3516  funeu2 3524  dffun6 3525  dffun8 3527  svrelfun 3546  fncnv 3547  funcnvuni 3550  imadif 3560  fcoi2 3631  fconst 3643  f11 3649  fores 3666  f1o4 3681  f1o5 3682  f1ocnv 3686  fvopab2 3776  eqfnfvf 3783  ffnfvf 3814  fsn2 3821  funiunfv 3851  f1fvf 3860  tfrlem2 3897  dfrdg2 3918  rdglem1 3922  tz7.49 3944  ffnoprval 3999  eqfnoprval 4001  fooprval 4022  2ndconst 4081  foprab2 4103  th3qlem1 4298  mapsnen 4410  xpassen 4421  pw2en 4426  xpmapenlem5 4480  abfii1 4535  abfii2 4536  inf2 4580  axinf 4595  trcl 4617  aceq1 4701  aceq3 4705  aceq4 4706  aceq5lem2 4708  aceq5lem3 4709  aceq5 4712  kmlem3 4739  kmlem4 4740  kmlem14 4750  kmlem15 4751  aceqkm 4753  zorn2lem7 4766  brdom7disj 4776  brdom6disj 4777  cf0 4882  zfcndrep 4938  zfcndinf 4942  distrlem1pr 5099  distrlem5pr 5103  opelreal 5221  elreal 5222  pre-axsup 5263  elnnz 6092  elznn0nn 6095  peano2uz2 6149  nnwof 6391  nnwos 6392  elfzuzb 6408  cau3ir 6852  cbvsum 6924  clm1 7015  climcmplem 7073  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  cvgratlem3 7187  elcncf1d 7205  ivth2OLD 7234  infpn2 7452  infmap2lem1 7521  infmap2 7523  istop2g 7539  istps4 7551  isbasis2g 7554  tgval2t 7559  tgval3t 7567  tgss3t 7580  basgent 7582  subtop 7588  fctop2 7593  clsval2 7627  cncnp 7717  blfval2 7776  blf 7784  iscau2 7875  xpcn 7910  oprcn 7911  fsumcnlem 7923  bcthlem4 7936  bcthlem12 7944  bcthlem14 7946  bcthlem32 7964  sspval 8316  ubthlem1 8460  spwval2 8577  spwmo 8580  pilem1 8590  axgroth4 8719  grothprim 8722  hlimcaui 9027  ocsh 9072  pjtheu 9150  shscl 9196  h1deot 9387  h1det 9388  hommvalt 9429  hfmmvalt 9432  nmcopexlem1 9866  nmcopexlem2 9867  nmcfnexlem1 9895  nmcfnexlem2 9896  pjhmopidm 10020  cvbr2t 10120  cvnbtwn2t 10124  cvnbtwn4t 10126  mdsl2 10157  cvmd 10159  mdsymlem6 10243  cdj3lem3b 10272  ahypfmbi 10326  eeeeanv 10336  infi 10448  ishgrag 10605

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