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 8669 lsmcv 19896 pmatcollpw2 21369 btwnconn1lem4 33558 linethru 33621 hlrelat3 36580 cvrval3 36581 cvrval4N 36582 2atlt 36607 atbtwnex 36616 1cvratlt 36642 atcvrlln2 36687 atcvrlln 36688 2llnmat 36692 lvolnlelpln 36753 lnjatN 36948 lncmp 36951 cdlemd9 37374 dihord5b 38427 dihmeetALTN 38495 mapdrvallem2 38813 itschlc0xyqsol 44839 |
Copyright terms: Public domain | W3C validator |