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

Theorem ex 148
Description: Exportation deduction.
Hypothesis
Ref Expression
ex.1 |- (R, S) |= T
Assertion
Ref Expression
ex |- R |= [S ==> T]

Proof of Theorem ex
StepHypRef Expression
1 wan 126 . . . 4 |- /\ :(* -> (* -> *))
2 ex.1 . . . . . 6 |- (R, S) |= T
32ax-cb1 29 . . . . 5 |- (R, S):*
43wctr 32 . . . 4 |- S:*
52ax-cb2 30 . . . 4 |- T:*
61, 4, 5wov 64 . . 3 |- [S /\ T]:*
73wctl 31 . . . 4 |- R:*
84, 5dfan2 144 . . . 4 |- T. |= [[S /\ T] = (S, T)]
97, 8a1i 28 . . 3 |- R |= [[S /\ T] = (S, T)]
104, 5wct 44 . . . . . 6 |- (S, T):*
117, 10simpr 23 . . . . 5 |- (R, (S, T)) |= (S, T)
1211simpld 35 . . . 4 |- (R, (S, T)) |= S
137, 4simpr 23 . . . . 5 |- (R, S) |= S
1413, 2jca 18 . . . 4 |- (R, S) |= (S, T)
1512, 14ded 74 . . 3 |- R |= [(S, T) = S]
166, 9, 15eqtri 85 . 2 |- R |= [[S /\ T] = S]
1716ax-cb1 29 . . 3 |- R:*
184, 5imval 136 . . 3 |- T. |= [[S ==> T] = [[S /\ T] = S]]
1917, 18a1i 28 . 2 |- R |= [[S ==> T] = [[S /\ T] = S]]
2016, 19mpbir 77 1 |- R |= [S ==> T]
Colors of variables: type var term
Syntax hints:  *hb 3   = ke 7  [kbr 9  kct 10   |= wffMMJ2 11   /\ tan 109   ==> tim 111
This theorem is referenced by:  notval2  149  notnot1  150  con2d  151  ecase  153  olc  154  orc  155  exlimdv2  156  exlimdv  157  ax4e  158  exlimd  171  alnex  174  isfree  176  exmid  186  ax1  190  ax2  191  ax3  192  ax5  194  ax7  196  ax8  198  ax10  200  ax11  201  ax12  202  ax13  203  ax14  204  axext  206  axrep  207  axpow  208  axun  209
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-refl 39  ax-eqmp 42  ax-ded 43  ax-ceq 46  ax-beta 60  ax-distrc 61  ax-leq 62  ax-distrl 63  ax-hbl1 93  ax-17 95  ax-inst 103
This theorem depends on definitions:  df-ov 65  df-an 118  df-im 119
  Copyright terms: Public domain W3C validator