![]() |
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 1193 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant1 1134 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 206 df-an 398 df-3an 1090 |
This theorem is referenced by: poxp3 8131 mapxpen 9139 lsmcv 20742 pmatcollpw2 22262 sltlpss 27381 btwnconn1lem4 35000 linethru 35063 hlrelat3 38221 cvrval3 38222 cvrval4N 38223 2atlt 38248 atbtwnex 38257 1cvratlt 38283 atcvrlln2 38328 atcvrlln 38329 2llnmat 38333 lvolnlelpln 38394 lnjatN 38589 lncmp 38592 cdlemd9 39015 dihord5b 40068 dihmeetALTN 40136 mapdrvallem2 40454 itschlc0xyqsol 47355 |
Copyright terms: Public domain | W3C validator |