**Description:** First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

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

Hypothesis | bnj1232.1 | $${\u22a2}{\phi}\leftrightarrow \left({\psi}\wedge {\chi}\wedge {\theta}\wedge {\tau}\right)$$ | |

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

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

1 | bnj1232.1 | $${\u22a2}{\phi}\leftrightarrow \left({\psi}\wedge {\chi}\wedge {\theta}\wedge {\tau}\right)$$ | |

2 | bnj642 | $${\u22a2}\left({\psi}\wedge {\chi}\wedge {\theta}\wedge {\tau}\right)\to {\psi}$$ | |

3 | 1 2 | sylbi | $${\u22a2}{\phi}\to {\psi}$$ |