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

---

Theorem mpd 146

Description: Modus ponens.

Hypotheses

Ref	Expression
mp.1
mp.2
mp.3

Assertion

Ref	Expression
mpd

---

Proof of Theorem mpd

Step	Hyp	Ref	Expression
1		mp.2	. . . 4
2		mp.3	. . . . 5
3	1	ax-cb1 29	. . . . . 6
4	1	ax-cb2 30	. . . . . . 7
5		mp.1	. . . . . . 7
6	4, 5	imval 136	. . . . . 6
7	3, 6	a1i 28	. . . . 5
8	2, 7	mpbi 72	. . . 4
9	1, 8	mpbir 77	. . 3
10	4, 5	dfan2 144	. . . 4
11	3, 10	a1i 28	. . 3
12	9, 11	mpbi 72	. 2
13	12	simprd 36	1

Colors of variables: type var term

Syntax hints:  hb 3   ke 7  kbr 9  kct 10   wffMMJ2 11  wffMMJ2t 12   tan 109   tim 111

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

This theorem is referenced by:  imp  147  notval2  149  notnot1  150  ecase  153  olc  154  orc  155  exlimdv2  156  ax4e  158  exlimd  171  ac  184  exmid  186  ax2  191  axmp  193  ax5  194  ax11  201

Copyright terms: Public domain

W3C validator