**Description:** An inference based on modus ponens. (Contributed by NM, 23-May-1999)
(Proof shortened by Wolf Lammen, 22-Nov-2012)

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

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

mpdan.2 | $${\u22a2}\left({\phi}\wedge {\psi}\right)\to {\chi}$$ | ||

Assertion | mpdan | $${\u22a2}{\phi}\to {\chi}$$ |

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

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

2 | mpdan.2 | $${\u22a2}\left({\phi}\wedge {\psi}\right)\to {\chi}$$ | |

3 | id | $${\u22a2}{\phi}\to {\phi}$$ | |

4 | 3 1 2 | syl2anc | $${\u22a2}{\phi}\to {\chi}$$ |