**Description:** Change disjunction in consequent to conjunction in antecedent.
(Contributed by NM, 8-Jun-1994)

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

Hypothesis | orcanai.1 | $${\u22a2}{\phi}\to \left({\psi}\vee {\chi}\right)$$ | |

Assertion | orcanai | $${\u22a2}\left({\phi}\wedge \neg {\psi}\right)\to {\chi}$$ |

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

1 | orcanai.1 | $${\u22a2}{\phi}\to \left({\psi}\vee {\chi}\right)$$ | |

2 | 1 | ord | $${\u22a2}{\phi}\to \left(\neg {\psi}\to {\chi}\right)$$ |

3 | 2 | imp | $${\u22a2}\left({\phi}\wedge \neg {\psi}\right)\to {\chi}$$ |