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

Theorem feq123d 6492
 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 6491 . 2 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))
4 feq123d.3 . . 3 (𝜑𝐶 = 𝐷)
54feq3d 6490 . 2 (𝜑 → (𝐺:𝐵𝐶𝐺:𝐵𝐷))
63, 5bitrd 282 1 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ⟶wf 6336 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-br 5037  df-opab 5099  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-fun 6342  df-fn 6343  df-f 6344 This theorem is referenced by:  feq123  6493  feq23d  6498  fprg  6914  csbwrdg  13956  funcestrcsetclem8  17476  funcsetcestrclem8  17491  funcsetcestrclem9  17492  evlfcl  17551  yonedalem3a  17603  yonedalem4c  17606  yonedalem3b  17608  yonedainv  17610  iscau  23989  isuhgr  26965  uhgreq12g  26970  isuhgrop  26975  uhgrun  26979  isupgr  26989  upgrop  26999  isumgr  27000  upgrun  27023  umgrun  27025  lfuhgr1v0e  27156  wlkp1  27583  sseqf  31890  ismfs  33039  isrngo  35649  gneispace2  41243  funcringcsetcALTV2lem8  45083  funcringcsetclem8ALTV  45106
 Copyright terms: Public domain W3C validator