**Description:** Weak deduction theorem that eliminates a hypothesis ph , making it
become an antecedent. We assume that a proof exists for ph when the
class variable A is replaced with a specific class B . The
hypothesis ch should be assigned to the inference, and the inference
hypothesis eliminated with elimhyp . If the inference has other
hypotheses with class variable A , these can be kept by assigning
keephyp to them. For more information, see the Weak Deduction Theorem
page mmdeduction.html . (Contributed by NM, 15-May-1999)

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

Hypotheses | dedth.1 | $${\u22a2}{A}=if\left({\phi},{A},{B}\right)\to \left({\psi}\leftrightarrow {\chi}\right)$$ | |

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

Assertion | dedth | $${\u22a2}{\phi}\to {\psi}$$ |

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

1 | dedth.1 | $${\u22a2}{A}=if\left({\phi},{A},{B}\right)\to \left({\psi}\leftrightarrow {\chi}\right)$$ | |

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

3 | iftrue | $${\u22a2}{\phi}\to if\left({\phi},{A},{B}\right)={A}$$ | |

4 | 3 | eqcomd | $${\u22a2}{\phi}\to {A}=if\left({\phi},{A},{B}\right)$$ |

5 | 4 1 | syl | $${\u22a2}{\phi}\to \left({\psi}\leftrightarrow {\chi}\right)$$ |

6 | 2 5 | mpbiri | $${\u22a2}{\phi}\to {\psi}$$ |