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

Theorem feq123d 6245
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 6244 . 2 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))
4 feq123d.3 . . 3 (𝜑𝐶 = 𝐷)
54feq3d 6243 . 2 (𝜑 → (𝐺:𝐵𝐶𝐺:𝐵𝐷))
63, 5bitrd 271 1 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1653  wf 6097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-br 4844  df-opab 4906  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-fun 6103  df-fn 6104  df-f 6105
This theorem is referenced by:  feq123  6246  feq23d  6251  fprg  6650  csbwrdg  13564  funcestrcsetclem8  17102  funcsetcestrclem8  17117  funcsetcestrclem9  17118  evlfcl  17177  yonedalem3a  17229  yonedalem4c  17232  yonedalem3b  17234  yonedainv  17236  iscau  23402  isuhgr  26295  uhgreq12g  26300  isuhgrop  26305  uhgrun  26309  isupgr  26319  upgrop  26329  isumgr  26330  upgrun  26353  umgrun  26355  lfuhgr1v0e  26488  wlkp1  26934  sseqf  30971  ismfs  31963  isrngo  34183  gneispace2  39212  funcringcsetcALTV2lem8  42842  funcringcsetclem8ALTV  42865
  Copyright terms: Public domain W3C validator