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 1065 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant1 1082 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: mapxpen 8126 lsmcv 19141 pmatcollpw2 20583 btwnconn1lem4 32197 linethru 32260 hlrelat3 34698 cvrval3 34699 cvrval4N 34700 2atlt 34725 atbtwnex 34734 1cvratlt 34760 atcvrlln2 34805 atcvrlln 34806 2llnmat 34810 lvolnlelpln 34871 lnjatN 35066 lncmp 35069 cdlemd9 35493 dihord5b 36548 dihmeetALTN 36616 mapdrvallem2 36934 |
Copyright terms: Public domain | W3C validator |