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

Theorem mpd 156
Description: Modus ponens. (Contributed by Mario Carneiro, 9-Oct-2014.)
Hypotheses
Ref Expression
mp.1 |- T:*
mp.2 |- R |= S
mp.3 |- R |= [S ==> T]
Assertion
Ref Expression
mpd |- R |= T

Proof of Theorem mpd
StepHypRef Expression
1 mp.2 . . . 4 |- R |= S
2 mp.3 . . . . 5 |- R |= [S ==> T]
31ax-cb1 29 . . . . . 6 |- R:*
41ax-cb2 30 . . . . . . 7 |- S:*
5 mp.1 . . . . . . 7 |- T:*
64, 5imval 146 . . . . . 6 |- T. |= [[S ==> T] = [[S /\ T] = S]]
73, 6a1i 28 . . . . 5 |- R |= [[S ==> T] = [[S /\ T] = S]]
82, 7mpbi 82 . . . 4 |- R |= [[S /\ T] = S]
91, 8mpbir 87 . . 3 |- R |= [S /\ T]
104, 5dfan2 154 . . . 4 |- T. |= [[S /\ T] = (S, T)]
113, 10a1i 28 . . 3 |- R |= [[S /\ T] = (S, T)]
129, 11mpbi 82 . 2 |- R |= (S, T)
1312simprd 38 1 |- R |= T
Colors of variables: type var term
Syntax hints:  *hb 3   = ke 7  [kbr 9  kct 10   |= wffMMJ2 11  wffMMJ2t 12   /\ 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:  imp  157  notval2  159  notnot1  160  ecase  163  olc  164  orc  165  exlimdv2  166  ax4e  168  exlimd  183  ac  197  exmid  199  ax2  204  axmp  206  ax5  207  ax11  214
  Copyright terms: Public domain W3C validator