ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fssd GIF version

Theorem fssd 5370
Description: Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fssd.f (𝜑𝐹:𝐴𝐵)
fssd.b (𝜑𝐵𝐶)
Assertion
Ref Expression
fssd (𝜑𝐹:𝐴𝐶)

Proof of Theorem fssd
StepHypRef Expression
1 fssd.f . 2 (𝜑𝐹:𝐴𝐵)
2 fssd.b . 2 (𝜑𝐵𝐶)
3 fss 5369 . 2 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
41, 2, 3syl2anc 411 1 (𝜑𝐹:𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 3127  wf 5204
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157
This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140  df-f 5212
This theorem is referenced by:  mapss  6681  ac6sfi  6888  fseq1p1m1  10062  resqrexlemcvg  10995  resqrexlemsqa  11000  climcvg1nlem  11324  fsumcl2lem  11373  ennnfonelemh  12371  cnrest2  13229  cnptoprest2  13233  cncfss  13563  limccnpcntop  13637  dvcoapbr  13664  dvef  13681  isomninnlem  14261  trilpolemisumle  14269  iswomninnlem  14280  ismkvnnlem  14283
  Copyright terms: Public domain W3C validator