| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simpl11 | 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 |
|---|---|
| simpl11 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl1 1192 | . 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 tsmsxp 24163 nolt02o 27740 nogt01o 27741 cofsslt 27952 brbtwn2 28920 ax5seg 28953 3vfriswmgr 30297 br8 35756 btwndiff 36028 ifscgr 36045 seglecgr12im 36111 lkrshp 39106 cvlcvr1 39340 atbtwn 39448 3dimlem3 39463 3dimlem3OLDN 39464 1cvratex 39475 llnmlplnN 39541 4atlem3 39598 4atlem3a 39599 4atlem11 39611 4atlem12 39614 lnatexN 39781 cdlemb 39796 paddasslem4 39825 paddasslem10 39831 pmodlem1 39848 llnexchb2lem 39870 llnexchb2 39871 arglem1N 40192 cdlemd4 40203 cdlemd9 40208 cdlemd 40209 cdleme16 40287 cdleme20 40326 cdleme21i 40337 cdleme21k 40340 cdleme27N 40371 cdleme28c 40374 cdlemefrs29bpre0 40398 cdlemefrs29clN 40401 cdlemefrs32fva 40402 cdleme41sn3a 40435 cdleme32fva 40439 cdleme40n 40470 cdlemg12e 40649 cdlemg15a 40657 cdlemg15 40658 cdlemg16ALTN 40660 cdlemg16z 40661 cdlemg20 40687 cdlemg22 40689 cdlemg29 40707 cdlemg38 40717 cdlemk33N 40911 cdlemk56 40973 dihord11b 41224 dihord2pre 41227 dihord4 41260 ismnu 44280 fourierdlem77 46198 |
| Copyright terms: Public domain | W3C validator |