Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simpl12 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpl12 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp12 1085 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) | |
2 | 1 | adantr 480 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: pythagtriplem4 15362 pmatcollpw1lem1 20398 pmatcollpw1 20400 mp2pm2mplem2 20431 brbtwn2 25585 ax5seg 25618 br8 30899 ifscgr 31321 seglecgr12im 31387 lkrshp 33410 atlatle 33625 cvlcvr1 33644 atbtwn 33750 3dimlem3 33765 3dimlem3OLDN 33766 1cvratex 33777 llnmlplnN 33843 4atlem3 33900 4atlem3a 33901 4atlem11 33913 4atlem12 33916 cdlemb 34098 paddasslem4 34127 paddasslem10 34133 pmodlem1 34150 llnexchb2lem 34172 arglem1N 34495 cdlemd4 34506 cdlemd 34512 cdleme16 34590 cdleme20 34630 cdleme21k 34644 cdleme22cN 34648 cdleme27N 34675 cdleme28c 34678 cdleme29ex 34680 cdleme32fva 34743 cdleme40n 34774 cdlemg15a 34961 cdlemg15 34962 cdlemg16ALTN 34964 cdlemg16z 34965 cdlemg20 34991 cdlemg22 34993 cdlemg29 35011 cdlemg38 35021 cdlemk33N 35215 cdlemk56 35277 fourierdlem77 39076 3vfriswmgr 41448 |
Copyright terms: Public domain | W3C validator |