HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ex GIF version

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⊧[ST]

Proof of Theorem ex
StepHypRef Expression
1 wan 136 . . . 4 :(∗ → (∗ → ∗))
2 ex.1 . . . . . 6 (R, S)⊧T
32ax-cb1 29 . . . . 5 (R, S):∗
43wctr 34 . . . 4 S:∗
52ax-cb2 30 . . . 4 T:∗
61, 4, 5wov 72 . . 3 [S T]:∗
73wctl 33 . . . 4 R:∗
84, 5dfan2 154 . . . 4 ⊤⊧[[S T] = (S, T)]
97, 8a1i 28 . . 3 R⊧[[S T] = (S, T)]
104, 5wct 48 . . . . . 6 (S, T):∗
117, 10simpr 23 . . . . 5 (R, (S, T))⊧(S, T)
1211simpld 37 . . . 4 (R, (S, T))⊧S
137, 4simpr 23 . . . . 5 (R, S)⊧S
1413, 2jca 18 . . . 4 (R, S)⊧(S, T)
1512, 14ded 84 . . 3 R⊧[(S, T) = S]
166, 9, 15eqtri 95 . 2 R⊧[[S T] = S]
1716ax-cb1 29 . . 3 R:∗
184, 5imval 146 . . 3 ⊤⊧[[ST] = [[S T] = S]]
1917, 18a1i 28 . 2 R⊧[[ST] = [[S T] = S]]
2016, 19mpbir 87 1 R⊧[ST]
Colors of variables: type var term
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
  Copyright terms: Public domain W3C validator