Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical implication
mpi
Metamath Proof Explorer
Theorem mpi
Description: A nested modus ponens inference. Inference associated with com12 .
(Contributed by NM , 29-Dec-1992) (Proof shortened by Stefan Allan , 20-Mar-2006)

Ref
Expression
Hypotheses
mpi.1
$${\u22a2}{\psi}$$
mpi.2
$${\u22a2}{\phi}\to \left({\psi}\to {\chi}\right)$$
Assertion
mpi
$${\u22a2}{\phi}\to {\chi}$$

Proof
Step
Hyp
Ref
Expression
1
mpi.1
$${\u22a2}{\psi}$$
2
mpi.2
$${\u22a2}{\phi}\to \left({\psi}\to {\chi}\right)$$
3
1
a1i
$${\u22a2}{\phi}\to {\psi}$$
4
3 2
mpd
$${\u22a2}{\phi}\to {\chi}$$