**Description:** A double modus ponens deduction. Deduction associated with mp2 .
(Contributed by NM, 23-May-2013) (Proof shortened by Wolf Lammen, 23-Jul-2013)

Ref | Expression | ||
---|---|---|---|

Hypotheses | mp2d.1 | $${\u22a2}{\phi}\to {\psi}$$ | |

mp2d.2 | $${\u22a2}{\phi}\to {\chi}$$ | ||

mp2d.3 | $${\u22a2}{\phi}\to \left({\psi}\to \left({\chi}\to {\theta}\right)\right)$$ | ||

Assertion | mp2d | $${\u22a2}{\phi}\to {\theta}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | mp2d.1 | $${\u22a2}{\phi}\to {\psi}$$ | |

2 | mp2d.2 | $${\u22a2}{\phi}\to {\chi}$$ | |

3 | mp2d.3 | $${\u22a2}{\phi}\to \left({\psi}\to \left({\chi}\to {\theta}\right)\right)$$ | |

4 | 2 3 | mpid | $${\u22a2}{\phi}\to \left({\psi}\to {\theta}\right)$$ |

5 | 1 4 | mpd | $${\u22a2}{\phi}\to {\theta}$$ |