| 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.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
| Ref | Expression |
|---|---|
| simpl12 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl2 1193 | . 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 pmatcollpw1lem1 22780 pmatcollpw1 22782 mp2pm2mplem2 22813 nolt02o 27740 nogt01o 27741 brbtwn2 28920 ax5seg 28953 3vfriswmgr 30297 br8 35756 ifscgr 36045 seglecgr12im 36111 lkrshp 39106 atlatle 39321 cvlcvr1 39340 atbtwn 39448 3dimlem3 39463 3dimlem3OLDN 39464 1cvratex 39475 llnmlplnN 39541 4atlem3 39598 4atlem3a 39599 4atlem11 39611 4atlem12 39614 cdlemb 39796 paddasslem4 39825 paddasslem10 39831 pmodlem1 39848 llnexchb2lem 39870 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 cdlemk33N 40911 cdlemk56 40973 fourierdlem77 46198 |
| Copyright terms: Public domain | W3C validator |