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 1463 | . 2 ⊢ ((𝜓 ∧ (𝜓 ∧ 𝜃)) → 𝜂) |
6 | 5 | anabss5 666 | 1 ⊢ ((𝜓 ∧ 𝜃) → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: sqrlem4 14605 gcdmultipleOLD 15900 coprm 16055 frlmssuvc1 20938 en2top 21593 tgrest 21767 pi1cof 23663 voliunlem1 24151 dvnfre 24549 dvcnvre 24616 ig1pdvds 24770 taylthlem2 24962 chtub 25788 2lgsoddprmlem2 25985 isosctrlem1ALT 41288 odz2prm2pw 43745 lighneallem4 43795 |
Copyright terms: Public domain | W3C validator |