![]() |
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 767 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant1 1130 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: lspsolvlem 21125 dmatcrng 22498 scmatcrng 22517 1marepvsma1 22579 mdetunilem7 22614 mat2pmatghm 22726 pmatcollpwscmatlem2 22786 mp2pm2mplem4 22805 ax5seg 28875 measinblem 34055 btwnconn1lem13 35925 athgt 39157 llnle 39219 lplnle 39241 lhpexle1 39709 lhpat3 39747 tendoicl 40497 cdlemk55b 40661 pellex 42510 ssfiunibd 44942 mullimc 45255 mullimcf 45262 icccncfext 45526 etransclem32 45905 uhgrimisgrgriclem 47495 |
Copyright terms: Public domain | W3C validator |