![]() |
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 759 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant1 1124 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: lspsolvlem 19538 dmatcrng 20713 scmatcrng 20732 1marepvsma1 20794 mdetunilem7 20829 mat2pmatghm 20942 pmatcollpwscmatlem2 21002 mp2pm2mplem4 21021 ax5seg 26287 measinblem 30881 btwnconn1lem13 32795 athgt 35612 llnle 35674 lplnle 35696 lhpexle1 36164 lhpat3 36202 tendoicl 36952 cdlemk55b 37116 pellex 38363 ssfiunibd 40436 mullimc 40760 mullimcf 40767 icccncfext 41032 etransclem32 41414 |
Copyright terms: Public domain | W3C validator |