Theorem ex 158

Description: Exportation deduction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Hypothesis

Ref	Expression
ex.1	⊢ (R, S)⊧T

Assertion

Ref	Expression
ex	⊢ R⊧[S ⇒ T]

Proof of Theorem ex

Step	Hyp	Ref	Expression
1		wan 136	. . . 4 ⊢ ∧ :(∗ → (∗ → ∗))
2		ex.1	. . . . . 6 ⊢ (R, S)⊧T
3	2	ax-cb1 29	. . . . 5 ⊢ (R, S):∗
4	3	wctr 34	. . . 4 ⊢ S:∗
5	2	ax-cb2 30	. . . 4 ⊢ T:∗
6	1, 4, 5	wov 72	. . 3 ⊢ [S ∧ T]:∗
7	3	wctl 33	. . . 4 ⊢ R:∗
8	4, 5	dfan2 154	. . . 4 ⊢ ⊤⊧[[S ∧ T] = (S, T)]
9	7, 8	a1i 28	. . 3 ⊢ R⊧[[S ∧ T] = (S, T)]
10	4, 5	wct 48	. . . . . 6 ⊢ (S, T):∗
11	7, 10	simpr 23	. . . . 5 ⊢ (R, (S, T))⊧(S, T)
12	11	simpld 37	. . . 4 ⊢ (R, (S, T))⊧S
13	7, 4	simpr 23	. . . . 5 ⊢ (R, S)⊧S
14	13, 2	jca 18	. . . 4 ⊢ (R, S)⊧(S, T)
15	12, 14	ded 84	. . 3 ⊢ R⊧[(S, T) = S]
16	6, 9, 15	eqtri 95	. 2 ⊢ R⊧[[S ∧ T] = S]
17	16	ax-cb1 29	. . 3 ⊢ R:∗
18	4, 5	imval 146	. . 3 ⊢ ⊤⊧[[S ⇒ T] = [[S ∧ T] = S]]
19	17, 18	a1i 28	. 2 ⊢ R⊧[[S ⇒ T] = [[S ∧ T] = S]]
20	16, 19	mpbir 87	1 ⊢ R⊧[S ⇒ T]

Syntax hints:  ∗hb 3   = ke 7  [kbr 9  kct 10  ⊧wffMMJ2 11   ∧ tan 119   ⇒ tim 121

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-id 24  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-wctl 31  ax-wctr 32  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-ded 46  ax-wct 47  ax-wc 49  ax-ceq 51  ax-wv 63  ax-wl 65  ax-beta 67  ax-distrc 68  ax-leq 69  ax-distrl 70  ax-wov 71  ax-eqtypi 77  ax-eqtypri 80  ax-hbl1 103  ax-17 105  ax-inst 113

This theorem depends on definitions:  df-ov 73  df-an 128  df-im 129

This theorem is referenced by:  notval2  159  notnot1  160  con2d  161  ecase  163  olc  164  orc  165  exlimdv2  166  exlimdv  167  ax4e  168  exlimd  183  alnex  186  isfree  188  exmid  199  ax1  203  ax2  204  ax3  205  ax5  207  ax7  209  ax8  211  ax10  213  ax11  214  ax12  215  ax13  216  ax14  217  axext  219  axrep  220  axpow  221  axun  222