| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mp3an2ani | Structured version Visualization version GIF version | ||
| Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) |
| Ref | Expression |
|---|---|
| mp3an2ani.1 | ⊢ 𝜑 |
| mp3an2ani.2 | ⊢ (𝜓 → 𝜒) |
| mp3an2ani.3 | ⊢ ((𝜓 ∧ 𝜃) → 𝜏) |
| mp3an2ani.4 | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) |
| Ref | Expression |
|---|---|
| mp3an2ani | ⊢ ((𝜓 ∧ 𝜃) → 𝜂) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mp3an2ani.1 | . . 3 ⊢ 𝜑 | |
| 2 | mp3an2ani.2 | . . 3 ⊢ (𝜓 → 𝜒) | |
| 3 | mp3an2ani.3 | . . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏) | |
| 4 | mp3an2ani.4 | . . 3 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) | |
| 5 | 1, 2, 3, 4 | mp3an3an 1469 | . 2 ⊢ ((𝜓 ∧ (𝜓 ∧ 𝜃)) → 𝜂) |
| 6 | 5 | anabss5 668 | 1 ⊢ ((𝜓 ∧ 𝜃) → 𝜂) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: 01sqrexlem4 15284 coprm 16748 frlmssuvc1 21814 en2top 22992 tgrest 23167 pi1cof 25092 voliunlem1 25585 dvnfre 25990 dvcnvre 26058 ig1pdvds 26219 taylthlem2 26416 taylthlem2OLD 26417 chtub 27256 2lgsoddprmlem2 27453 fzo0opth 32807 nsgmgc 33440 omabs2 43345 isosctrlem1ALT 44954 odz2prm2pw 47550 lighneallem4 47597 itcovalpclem2 48592 itcovalt2lem2 48597 |
| Copyright terms: Public domain | W3C validator |