| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simpl13 | 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 |
|---|---|
| simpl13 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl3 1194 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒) | |
| 2 | 1 | 3ad2antl1 1186 | 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: pythagtriplem4 16857 mply1topmatcl 22811 nolt02o 27740 nogt01o 27741 cofsslt 27952 coinitsslt 27953 brbtwn2 28920 ax5seg 28953 br8 35756 btwndiff 36028 ifscgr 36045 seglecgr12im 36111 atlatle 39321 cvlcvr1 39340 atbtwn 39448 3dimlem3 39463 3dimlem3OLDN 39464 4atlem3 39598 4atlem11 39611 4atlem12 39614 2lplnj 39622 paddasslem4 39825 paddasslem10 39831 pmodlem1 39848 llnexchb2lem 39870 pclfinclN 39952 arglem1N 40192 cdlemd4 40203 cdlemd 40209 cdleme16 40287 cdleme20 40326 cdleme21k 40340 cdleme22cN 40344 cdleme27N 40371 cdleme28c 40374 cdleme29ex 40376 cdleme32fva 40439 cdleme40n 40470 cdlemg15a 40657 cdlemg15 40658 cdlemg16ALTN 40660 cdlemg16z 40661 cdlemg20 40687 cdlemg22 40689 cdlemg29 40707 cdlemg38 40717 cdlemk56 40973 dihord2pre 41227 ismnu 44280 uzwo4 45058 fourierdlem77 46198 |
| Copyright terms: Public domain | W3C validator |