| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp1rr | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| Ref | Expression |
|---|---|
| simp1rr | ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simprr 773 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
| 2 | 1 | 3ad2ant1 1134 | 1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: f1imass 7284 smo11 8404 zsupss 12979 lsmcv 21143 lspsolvlem 21144 mat2pmatghm 22736 mat2pmatmul 22737 nrmr0reg 23757 plyadd 26256 plymul 26257 coeeu 26264 ax5seglem6 28949 archiabl 33205 mdetpmtr1 33822 sseqval 34390 wsuclem 35826 btwnconn1lem1 36088 btwnconn1lem2 36089 btwnconn1lem12 36099 lshpsmreu 39110 1cvratlt 39476 llnle 39520 lvolex3N 39540 lnjatN 39782 lncvrat 39784 lncmp 39785 cdlemd6 40205 cdlemk19ylem 40932 pellex 42846 tfsconcatrn 43355 limcperiod 45643 itschlc0xyqsol1 48687 itschlc0xyqsol 48688 |
| Copyright terms: Public domain | W3C validator |