Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp1lr | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp1lr | ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplr 766 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant1 1132 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 |
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 397 df-3an 1088 |
This theorem is referenced by: lspsolvlem 20404 dmatcrng 21651 scmatcrng 21670 1marepvsma1 21732 mdetunilem7 21767 mat2pmatghm 21879 pmatcollpwscmatlem2 21939 mp2pm2mplem4 21958 ax5seg 27306 measinblem 32188 btwnconn1lem13 34401 athgt 37470 llnle 37532 lplnle 37554 lhpexle1 38022 lhpat3 38060 tendoicl 38810 cdlemk55b 38974 pellex 40657 ssfiunibd 42848 mullimc 43157 mullimcf 43164 icccncfext 43428 etransclem32 43807 |
Copyright terms: Public domain | W3C validator |