Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp1rl | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp1rl | ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprl 790 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2ant1 1075 | 1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: f1imass 6422 smo11 7348 zsupss 11653 lsmcv 18962 lspsolvlem 18963 mat2pmatghm 20354 mat2pmatmul 20355 plyadd 23777 plymul 23778 coeeu 23785 aannenlem1 23887 logexprlim 24750 ax5seglem6 25614 ax5seg 25618 mdetpmtr1 29217 mdetpmtr2 29218 wsuclem 31017 wsuclemOLD 31018 btwnconn1lem2 31365 btwnconn1lem3 31366 btwnconn1lem4 31367 btwnconn1lem12 31375 lshpsmreu 33414 2llnmat 33828 lvolex3N 33842 lnjatN 34084 pclfinclN 34254 lhpat3 34350 cdlemd6 34508 cdlemfnid 34870 cdlemk19ylem 35236 dihlsscpre 35541 dih1dimb2 35548 dihglblem6 35647 pellex 36417 mullimc 38683 mullimcf 38690 limcperiod 38695 cncfshift 38759 cncfperiod 38764 |
Copyright terms: Public domain | W3C validator |