MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq123d Structured version   Visualization version   GIF version

Theorem feq123d 6726
Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypotheses
Ref Expression
feq12d.1 (𝜑𝐹 = 𝐺)
feq12d.2 (𝜑𝐴 = 𝐵)
feq123d.3 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
feq123d (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐷))

Proof of Theorem feq123d
StepHypRef Expression
1 feq12d.1 . . 3 (𝜑𝐹 = 𝐺)
2 feq12d.2 . . 3 (𝜑𝐴 = 𝐵)
31, 2feq12d 6725 . 2 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))
4 feq123d.3 . . 3 (𝜑𝐶 = 𝐷)
54feq3d 6724 . 2 (𝜑 → (𝐺:𝐵𝐶𝐺:𝐵𝐷))
63, 5bitrd 279 1 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1537  wf 6559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-fun 6565  df-fn 6566  df-f 6567
This theorem is referenced by:  feq123  6727  feq23d  6732  fprg  7175  csbwrdg  14579  funcestrcsetclem8  18203  funcsetcestrclem8  18218  funcsetcestrclem9  18219  evlfcl  18279  yonedalem3a  18331  yonedalem4c  18334  yonedalem3b  18336  yonedainv  18338  iscau  25324  isuhgr  29092  uhgreq12g  29097  isuhgrop  29102  uhgrun  29106  isupgr  29116  upgrop  29126  isumgr  29127  upgrun  29150  umgrun  29152  lfuhgr1v0e  29286  wlkp1  29714  sseqf  34374  ismfs  35534  isrngo  37884  gneispace2  44122  isubgruhgr  47792  funcringcsetcALTV2lem8  48141  funcringcsetclem8ALTV  48164
  Copyright terms: Public domain W3C validator