**Description:** An inference based on modus ponens. (Contributed by NM, 12-Dec-2004)

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

Hypotheses | mp2ani.1 | $${\u22a2}{\psi}$$ | |

mp2ani.2 | $${\u22a2}{\chi}$$ | ||

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

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

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

1 | mp2ani.1 | $${\u22a2}{\psi}$$ | |

2 | mp2ani.2 | $${\u22a2}{\chi}$$ | |

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

4 | 1 3 | mpani | $${\u22a2}{\phi}\to \left({\chi}\to {\theta}\right)$$ |

5 | 2 4 | mpi | $${\u22a2}{\phi}\to {\theta}$$ |