![]() |
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 1466 | . 2 ⊢ ((𝜓 ∧ (𝜓 ∧ 𝜃)) → 𝜂) |
6 | 5 | anabss5 668 | 1 ⊢ ((𝜓 ∧ 𝜃) → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: 01sqrexlem4 15281 coprm 16745 frlmssuvc1 21832 en2top 23008 tgrest 23183 pi1cof 25106 voliunlem1 25599 dvnfre 26005 dvcnvre 26073 ig1pdvds 26234 taylthlem2 26431 taylthlem2OLD 26432 chtub 27271 2lgsoddprmlem2 27468 fzo0opth 32813 nsgmgc 33420 omabs2 43322 isosctrlem1ALT 44932 odz2prm2pw 47488 lighneallem4 47535 itcovalpclem2 48521 itcovalt2lem2 48526 |
Copyright terms: Public domain | W3C validator |