**Description:** Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011)

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

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

Assertion | simp3bi | $${\u22a2}{\phi}\to {\theta}$$ |

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

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

2 | 1 | biimpi | $${\u22a2}{\phi}\to \left({\psi}\wedge {\chi}\wedge {\theta}\right)$$ |

3 | 2 | simp3d | $${\u22a2}{\phi}\to {\theta}$$ |