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

Theorem feq123d 6658
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 6657 . 2 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))
4 feq123d.3 . . 3 (𝜑𝐶 = 𝐷)
54feq3d 6656 . 2 (𝜑 → (𝐺:𝐵𝐶𝐺:𝐵𝐷))
63, 5bitrd 279 1 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wf 6493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-fun 6499  df-fn 6500  df-f 6501
This theorem is referenced by:  feq123  6659  feq23d  6664  fprg  7102  csbwrdg  14438  funcestrcsetclem8  18040  funcsetcestrclem8  18055  funcsetcestrclem9  18056  evlfcl  18116  yonedalem3a  18168  yonedalem4c  18171  yonedalem3b  18173  yonedainv  18175  iscau  24656  isuhgr  28053  uhgreq12g  28058  isuhgrop  28063  uhgrun  28067  isupgr  28077  upgrop  28087  isumgr  28088  upgrun  28111  umgrun  28113  lfuhgr1v0e  28244  wlkp1  28671  sseqf  33049  ismfs  34200  isrngo  36402  gneispace2  42492  funcringcsetcALTV2lem8  46427  funcringcsetclem8ALTV  46450
  Copyright terms: Public domain W3C validator