Theorem feq123d 6676

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

Step	Hyp	Ref	Expression
1		feq12d.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2		feq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	feq12d 6675	. 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶))
4		feq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
5	4	feq3d 6672	. 2 ⊢ (𝜑 → (𝐺:𝐵⟶𝐶 ↔ 𝐺:𝐵⟶𝐷))
6	3, 5	bitrd 281	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐷))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  ⟶wf 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-fun 6519  df-fn 6520  df-f 6521

This theorem is referenced by:  feq123  6677  feq23d  6682  fprg  7134  csbwrdg  14554  funcestrcsetclem8  18162  funcsetcestrclem8  18177  funcsetcestrclem9  18178  evlfcl  18237  yonedalem3a  18289  yonedalem4c  18292  yonedalem3b  18294  yonedainv  18296  iscau  25318  isuhgr  29207  uhgreq12g  29212  isuhgrop  29217  uhgrun  29221  isupgr  29231  upgrop  29241  isumgr  29242  upgrun  29265  umgrun  29267  lfuhgr1v0e  29401  wlkp1  29826  sseqf  34650  ismfs  35863  isrngo  38360  gneispace2  44672  isubgruhgr  48454  funcringcsetcALTV2lem8  48883  funcringcsetclem8ALTV  48906