Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp1l2 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp1l2 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl2 1188 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant1 1129 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: mapxpen 8685 lsmcv 19915 pmatcollpw2 21388 btwnconn1lem4 33553 linethru 33616 hlrelat3 36550 cvrval3 36551 cvrval4N 36552 2atlt 36577 atbtwnex 36586 1cvratlt 36612 atcvrlln2 36657 atcvrlln 36658 2llnmat 36662 lvolnlelpln 36723 lnjatN 36918 lncmp 36921 cdlemd9 37344 dihord5b 38397 dihmeetALTN 38465 mapdrvallem2 38783 itschlc0xyqsol 44761 |
Copyright terms: Public domain | W3C validator |