| 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 1192 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑) | |
| 2 | 1 | 3ad2antl2 1187 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 1089 |
| This theorem is referenced by: frrlem10 8320 nosupbnd2lem1 27760 noinfbnd2lem1 27775 brbtwn2 28920 ax5seglem3a 28945 ax5seg 28953 axpasch 28956 axeuclid 28978 br8d 32622 br8 35756 cgrextend 36009 segconeq 36011 trisegint 36029 ifscgr 36045 cgrsub 36046 cgrxfr 36056 lineext 36077 seglecgr12im 36111 segletr 36115 lineunray 36148 lineelsb2 36149 cvrcmp 39284 cvlatexch3 39339 cvlsupr2 39344 atexchcvrN 39442 3dim1 39469 3dim2 39470 ps-1 39479 ps-2 39480 3atlem3 39487 3atlem5 39489 lplnnle2at 39543 lplnllnneN 39558 2llnjaN 39568 4atlem3 39598 4atlem10b 39607 4atlem12 39614 2llnma3r 39790 paddasslem4 39825 paddasslem7 39828 paddasslem8 39829 paddasslem12 39833 paddasslem13 39834 pmodlem1 39848 pmodlem2 39849 llnexchb2lem 39870 4atex2 40079 ltrnatlw 40185 trlval4 40190 arglem1N 40192 cdlemd4 40203 cdlemd5 40204 cdleme0moN 40227 cdleme16 40287 cdleme20 40326 cdleme21j 40338 cdleme21k 40340 cdleme27N 40371 cdleme28c 40374 cdleme43fsv1snlem 40422 cdleme38n 40466 cdleme40n 40470 cdleme41snaw 40478 cdlemg6c 40622 cdlemg8c 40631 cdlemg8 40633 cdlemg12e 40649 cdlemg16 40659 cdlemg16ALTN 40660 cdlemg16z 40661 cdlemg16zz 40662 cdlemg18a 40680 cdlemg20 40687 cdlemg22 40689 cdlemg37 40691 cdlemg27b 40698 cdlemg31d 40702 cdlemg33 40713 cdlemg38 40717 cdlemg44b 40734 cdlemk38 40917 cdlemk35s-id 40940 cdlemk39s-id 40942 cdlemk55 40963 cdlemk35u 40966 cdlemk55u 40968 cdleml3N 40980 cdlemn11pre 41212 |
| Copyright terms: Public domain | W3C validator |