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

Theorem feq123d 6706
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 6705 . 2 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))
4 feq123d.3 . . 3 (𝜑𝐶 = 𝐷)
54feq3d 6704 . 2 (𝜑 → (𝐺:𝐵𝐶𝐺:𝐵𝐷))
63, 5bitrd 278 1 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wf 6539
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-fun 6545  df-fn 6546  df-f 6547
This theorem is referenced by:  feq123  6707  feq23d  6712  fprg  7152  csbwrdg  14493  funcestrcsetclem8  18098  funcsetcestrclem8  18113  funcsetcestrclem9  18114  evlfcl  18174  yonedalem3a  18226  yonedalem4c  18229  yonedalem3b  18231  yonedainv  18233  iscau  24792  isuhgr  28317  uhgreq12g  28322  isuhgrop  28327  uhgrun  28331  isupgr  28341  upgrop  28351  isumgr  28352  upgrun  28375  umgrun  28377  lfuhgr1v0e  28508  wlkp1  28935  sseqf  33386  ismfs  34535  isrngo  36760  gneispace2  42873  funcringcsetcALTV2lem8  46931  funcringcsetclem8ALTV  46954
  Copyright terms: Public domain W3C validator