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 1458 | . 2 ⊢ ((𝜓 ∧ (𝜓 ∧ 𝜃)) → 𝜂) |
6 | 5 | anabss5 664 | 1 ⊢ ((𝜓 ∧ 𝜃) → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: sqrlem4 14593 gcdmultipleOLD 15888 coprm 16043 frlmssuvc1 20866 en2top 21521 tgrest 21695 pi1cof 23590 voliunlem1 24078 dvnfre 24476 dvcnvre 24543 ig1pdvds 24697 taylthlem2 24889 chtub 25715 2lgsoddprmlem2 25912 isosctrlem1ALT 41145 odz2prm2pw 43602 lighneallem4 43652 |
Copyright terms: Public domain | W3C validator |