Theorem mpii 43

Description: A doubly nested modus ponens inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 31-Jul-2012.)

Hypotheses

Ref	Expression
mpii.1
mpii.2

Assertion

Ref	Expression
mpii

Proof of Theorem mpii

Step	Hyp	Ref	Expression
1		mpii.1	. . 3
2	1	a1i 11	. 2
3		mpii.2	. 2
4	2, 3	mpdi 42	1

Syntax hints:  ->wi 4

This theorem is referenced by:  intmin  4306  dfiin2g  4363  ssorduni  6621  suceloni  6648  lublecllem  15618  irredmul  17358  opnneiid  19627  isufil2  20409  mdbr3  27216  mdbr4  27217  dmdbr5  27227  filnetlem4  30199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7