Theorem anbi1d 469

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

Hypothesis

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

Assertion

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

Proof of Theorem anbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	anbi2d 468	. 2 |- (ph -> ((th /\ ps) <-> (th /\ ch)))
3		ancom 333	. 2 |- ((ps /\ th) <-> (th /\ ps))
4		ancom 333	. 2 |- ((ch /\ th) <-> (th /\ ch))
5	2, 3, 4	3bitr4g 428	1 |- (ph -> ((ps /\ th) <-> (ch /\ th)))

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

This theorem is referenced by:  bibi2d 470  anbi12d 476  bi2anan9 478  axinf 1084  axac 1085  eleq1 1149  rexeqf 1322  reueqf 1323  rabeqf 1345  eqvinc 1407  alexeq 1409  ceqex 1410  axrep 1473  axrep2 1474  zfrepclf 1477  zfaus 1480  psstr 1574  difeq1 1582  ineq1 1638  r19.28zv 1769  raaan 1775  ifeq1 1778  ifeq2 1779  otthg 1900  copsexg 1902  copsex4g 1904  eluni 1922  reuuni2 1956  elopab 2110  pocl 2132  ordtri4 2235  dflim2 2280  xpeq1 2440  vtoclr 2449  opelxp 2452  opbrop 2472  coeq2 2503  opelco 2509  opelcog 2511  elxp4 2640  elxp5 2641  feq2 2749  f1eq2 2777  f1eq3 2778  foeq2 2785  dmfco 2864  fvco 2865  isoeq5 2929  isoini 2938  f1oiso 2942  tz7.44-1 2966  rdglem2 2976  eloprabg 3035  oprabval 3047  oprabvalig 3048  oprabval3 3052  ertr 3211  brecop 3242  ecopoprtrn 3247  th3qlem2 3251  th3q 3253  dom2d 3307  xpsnen 3339  xpassen 3344  pw2en 3348  mapxpen 3390  unfilem3 3440  preleq 3454  inf0 3457  r1pwcl 3530  aceq1 3552  aceq0 3553  aceq6a 3564  unxpdom 3650  cardcf 3706  cfsuc 3709  axrepnd 3740  axunndlem1 3741  axinfnd 3752  axacndlem5 3757  axacnd 3758  zfcndrep 3760  zfcndinf 3764  zfcndac 3765  ltsopq 3869  ltrpq 3879  genpass 3906  distrlem1pr 3921  distrlem5pr 3925  ltprord 3928  reclem2pr 3951  reclem3pr 3952  recexpr 3954  ltsosr 3997  mulgt0sr 4008  ltresr 4052  ltsor 4055  axmulgt0 4086  lt2addt 4361  addge0t 4362  mulge0t 4375  divgt0t 4402  divge0t 4403  ltrect 4417  lerect 4418  ltdiv23t 4419  le2sqt 4420  crut 4531  uzind 4603  qbtwnre 4650  sqe11t 4705  lt2sqet 4706  nn0opth2t 4726  sqrlem12 4742  sqr00t 4770  sqr2irrlem2 4778  abs3lemt 4865  clim 4877  clim2 4881  climunii 4883  climuni 4884  ruclem12 4896  norm3lemt 5097  hlim 5108  hlim2 5112  closedsub 5128  hlimunii 5143  hlimuni 5144  occllem8 5187  projlem1 5193  projlem7 5199  projlem20 5212  shlubt 5355  cmbrt 5494  cvbrt 5714  mdbr 5726  chrelat2t 5761  mdsymlem2 5777

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