**Description:** Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995)

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

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

Assertion | orim1d | $${\u22a2}{\phi}\to \left(\left({\psi}\vee {\theta}\right)\to \left({\chi}\vee {\theta}\right)\right)$$ |

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

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

2 | idd | $${\u22a2}{\phi}\to \left({\theta}\to {\theta}\right)$$ | |

3 | 1 2 | orim12d | $${\u22a2}{\phi}\to \left(\left({\psi}\vee {\theta}\right)\to \left({\chi}\vee {\theta}\right)\right)$$ |