![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl21 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
Ref | Expression |
---|---|
simpl21 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 1190 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑) | |
2 | 1 | 3ad2antl2 1185 | 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: frrlem10 8318 nosupbnd2lem1 27774 noinfbnd2lem1 27789 brbtwn2 28934 ax5seglem3a 28959 ax5seg 28967 axpasch 28970 axeuclid 28992 br8d 32629 br8 35735 cgrextend 35989 segconeq 35991 trisegint 36009 ifscgr 36025 cgrsub 36026 cgrxfr 36036 lineext 36057 seglecgr12im 36091 segletr 36095 lineunray 36128 lineelsb2 36129 cvrcmp 39264 cvlatexch3 39319 cvlsupr2 39324 atexchcvrN 39422 3dim1 39449 3dim2 39450 ps-1 39459 ps-2 39460 3atlem3 39467 3atlem5 39469 lplnnle2at 39523 lplnllnneN 39538 2llnjaN 39548 4atlem3 39578 4atlem10b 39587 4atlem12 39594 2llnma3r 39770 paddasslem4 39805 paddasslem7 39808 paddasslem8 39809 paddasslem12 39813 paddasslem13 39814 pmodlem1 39828 pmodlem2 39829 llnexchb2lem 39850 4atex2 40059 ltrnatlw 40165 trlval4 40170 arglem1N 40172 cdlemd4 40183 cdlemd5 40184 cdleme0moN 40207 cdleme16 40267 cdleme20 40306 cdleme21j 40318 cdleme21k 40320 cdleme27N 40351 cdleme28c 40354 cdleme43fsv1snlem 40402 cdleme38n 40446 cdleme40n 40450 cdleme41snaw 40458 cdlemg6c 40602 cdlemg8c 40611 cdlemg8 40613 cdlemg12e 40629 cdlemg16 40639 cdlemg16ALTN 40640 cdlemg16z 40641 cdlemg16zz 40642 cdlemg18a 40660 cdlemg20 40667 cdlemg22 40669 cdlemg37 40671 cdlemg27b 40678 cdlemg31d 40682 cdlemg33 40693 cdlemg38 40697 cdlemg44b 40714 cdlemk38 40897 cdlemk35s-id 40920 cdlemk39s-id 40922 cdlemk55 40943 cdlemk35u 40946 cdlemk55u 40948 cdleml3N 40960 cdlemn11pre 41192 |
Copyright terms: Public domain | W3C validator |