Theorem opreq12d 3014

Description: Equality deduction for operations.

Hypotheses

Ref	Expression
opreq1d.1	⊢ (φ → A = B)
opreq12d.2	⊢ (φ → C = D)

Assertion

Ref	Expression
opreq12d	⊢ (φ → (AFC) = (BFD))

Proof of Theorem opreq12d

Step	Hyp	Ref	Expression
1		opreq1d.1	. . 3 ⊢ (φ → A = B)
2	1	opreq1d 3012	. 2 ⊢ (φ → (AFC) = (BFC))
3		opreq12d.2	. . 3 ⊢ (φ → C = D)
4	3	opreq2d 3013	. 2 ⊢ (φ → (BFC) = (BFD))
5	2, 4	eqtrd 1128	1 ⊢ (φ → (AFC) = (BFD))

Syntax hints:   → wi 2   = wceq 1091  (class class class)co 3001

This theorem is referenced by:  caoprdistr 3073  oesuc 3134  nnmsucr 3182  ecoprdi 3257  ltaddpq 3873  halfpq 3876  prlem934a 3931  prlem936a 3947  axrecex 4079  adddirt 4103  subdit 4184  divcan1z 4226  divcan2z 4227  divcan1t 4228  divcan2t 4229  recidt 4235  divdistrz 4245  divdistrt 4246  divcan3z 4249  divcan3t 4251  divadddivt 4264  ltsqt 4376  2timest 4490  seqrval 4664  seqsuclem 4669  discrlem2 4714  discrlem3 4715  discrlem 4716  nn0opth 4724  nn0opth2t 4726  sqrlem21 4751  sqrth 4757  cjvalt 4799  absvalt 4801  abslem2 4867  facp1t 4873  ruclem4 4888  xpnnen 4927  hvsub4t 5014  his7 5051  normlem6 5068  normlem7t 5072  bcseq 5073  normpyth 5090  hcauchy 5103  pjthlem7 5231  pjthlem8 5232  axpjpjt 5260  elspansn2t 5472  hosvalt 5489  hodvalt 5490  cmbrt 5494  pjcjt2 5580  hosdir 5609  hoddir 5610  pjsdi 5625  pjddi 5626  pjssmt 5635  pjssge0t 5636  pjdifnormt 5637  pjclem1 5649  pjc 5654  pjopytht 5662  stelt 5671  golem1 5704

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-xp 2424  df-cnv 2426  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fv 2438  df-opr 3003

metamath.org