Theorem wc 50

Description: The type of a combination. (Contributed by Mario Carneiro, 7-Oct-2014.)

Hypotheses

Ref	Expression
wc.1	⊢ F:(α → β)
wc.2	⊢ T:α

Assertion

Ref	Expression
wc	⊢ (FT):β

Proof of Theorem wc

Step	Hyp	Ref	Expression
1		wc.1	. 2 ⊢ F:(α → β)
2		wc.2	. 2 ⊢ T:α
3	1, 2	ax-wc 49	1 ⊢ (FT):β

Syntax hints:   → ht 2  kc 5  wffMMJ2t 12

This theorem was proved from axioms:  ax-wc 49

This theorem is referenced by:  eqcomx  52  ceq12  88  beta  92  distrc  93  distrl  94  eqtri  95  oveq123  98  hbxfrf  107  hbc  110  hbov  111  hbl  112  clf  115  ovl  117  wfal  135  wex  139  wor  140  weu  141  alval  142  exval  143  euval  144  notval  145  orval  147  ax4g  149  dfan2  154  notval2  159  notnot1  160  con3d  162  exlimdv2  166  exlimdv  167  ax4e  168  eta  178  cbvf  179  leqf  181  exlimd  183  alimdv  184  alnex  186  exnal1  187  ac  197  dfex2  198  exmid  199  notnot  200  exnal  201  ax3  205  ax5  207  ax6  208  ax7  209  ax9  212  ax10  213  ax11  214  ax12  215  ax13  216  ax14  217  axext  219  axrep  220  axpow  221  axun  222