Theorem anbi2d 468

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

Hypothesis

Ref	Expression
bid.1	|- (ph -> (ps <-> ch))

Assertion

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

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . . 4 |- (ph -> (ps <-> ch))
2	1	biimpd 135	. . 3 |- (ph -> (ps -> ch))
3	2	anim2d 433	. 2 |- (ph -> ((th /\ ps) -> (th /\ ch)))
4	1	biimprd 136	. . 3 |- (ph -> (ch -> ps))
5	4	anim2d 433	. 2 |- (ph -> ((th /\ ch) -> (th /\ ps)))
6	3, 5	impbid 397	1 |- (ph -> ((th /\ ps) <-> (th /\ ch)))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  anbi1d 469  bibi2d 470  anbi12d 476  bi2anan9 478  axac 1085  eleq2 1150  eqvinc 1407  moeq3 1432  sbc5g 1450  difeq2 1583  undif4 1744  r19.27zv 1771  raaan 1775  opthg 1899  unieq 1927  biopabd 2101  pocl 2132  so 2152  ordelord 2221  limsuc 2361  xpeq2 2441  vtoclr 2449  opelxpg 2454  opbrop 2472  coeq1 2502  opelco 2509  opelcog 2511  iss 2599  elxp4 2640  elxp5 2641  fununi 2705  fneq2 2719  fneu 2728  fnun 2730  feq3 2750  fcoi1 2765  foeq3 2786  funbrfv 2852  fnopabfv 2858  fvco 2865  fvopab3 2868  fvopab3ig 2869  fvrn 2888  isoeq2 2926  isoeq3 2927  isoini 2938  f1oiso 2942  tfrlem1 2949  tz7.44-1 2966  tz7.44-2 2967  tz7.44-3 2968  rdgeq1 2972  rdgeq2 2973  bioprabd 3025  cbvoprab3v 3030  fnoprval 3042  oprabval 3047  oprabvalig 3048  oprabval3 3052  ertr 3211  elqsi 3228  brecop 3242  ecopoprtrn 3247  th3qlem1 3250  th3qlem2 3251  th3q 3253  domeng 3285  dom2d 3307  xpassen 3344  xpdom2 3345  pw2en 3348  mapxpen 3390  unfilem3 3440  fiint 3445  inf0 3457  scott0 3542  aceq1 3552  aceq0 3553  aceq2 3554  aceq3lem 3555  aceq3 3556  aceq5lem1 3558  aceq6b 3565  ac6 3576  kmlem13 3592  kmlem14 3593  unxpdom 3650  iscard2 3660  cfval 3701  axrepndlem1 3738  axunndlem1 3741  axregnd 3750  axinfndlem1 3751  axacndlem4 3756  axacndlem5 3757  zfcndac 3765  ltsopq 3869  prcdpq 3891  prnmax 3893  genpv 3896  genpelv 3897  genpprecl 3898  genpnnp 3902  genpnmax 3904  distrlem1pr 3921  ltprord 3928  ltexprlem3 3938  ltexprlem4 3939  ltexpri 3943  reclem2pr 3951  ltsosr 3997  mulgt0sr 4008  map2psrpr 4014  suppsr 4016  supsrlem6 4024  ltresr 4052  supre 4054  ltsor 4055  axnegex 4078  axmulgt0 4086  lenltt 4285  lt2addt 4361  addge0t 4362  lesub0t 4374  mulge0t 4375  divgt0t 4402  divge0t 4403  ltrect 4417  lerect 4418  ltdiv23t 4419  le2sqt 4420  crut 4531  uzwo 4605  nnwoOLD 4608  zbtwnre 4619  seqval 4665  sqe11t 4705  lt2sqet 4706  nn0opth2t 4726  sqrval 4729  abs3lemt 4865  clim 4877  clim2 4881  climuni 4884  ruclem12 4896  infxpidmlem2 4934  infmap2lem1 4951  infmap2 4953  norm3lemt 5097  hlim 5108  hlim2 5112  chlim 5139  hlimcaui 5141  hlimuni 5144  ocsh 5164  occllem8 5187  projlem7 5199  projlem20 5212  pjmvalt 5245  shlubt 5355  hosmvalt 5487  hodmvalt 5488  cmbrt 5494  spansncvt 5543  cvbrt 5714  mdbr 5726  atom1d 5750  chrelat2t 5761  atcvat 5771  atcvat2t 5773  mdsymlem5 5780

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