| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp2rr | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| Ref | Expression |
|---|---|
| simp2rr | ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simprr 773 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
| 2 | 1 | 3ad2ant2 1135 | 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: fpr3g 8310 tfrlem5 8420 omeu 8623 gruina 10858 4sqlem18 17000 vdwlem10 17028 mdetuni0 22627 mdetmul 22629 tsmsxp 24163 ax5seglem3 28946 btwnconn1lem1 36088 btwnconn1lem3 36090 btwnconn1lem4 36091 btwnconn1lem5 36092 btwnconn1lem6 36093 btwnconn1lem7 36094 btwnconn1lem12 36099 linethru 36154 2llnjN 39569 2lplnja 39621 2lplnj 39622 cdlemblem 39795 dalaw 39888 pclfinN 39902 lhpmcvr4N 40028 cdlemb2 40043 cdleme01N 40223 cdleme0ex2N 40226 cdleme7c 40247 cdlemefrs29bpre0 40398 cdlemefrs29cpre1 40400 cdlemefrs32fva1 40403 cdlemefs32sn1aw 40416 cdleme41sn3a 40435 cdleme48fv 40501 cdlemk21-2N 40893 dihmeetlem13N 41321 pellex 42846 lmhmfgsplit 43098 iunrelexpmin1 43721 |
| Copyright terms: Public domain | W3C validator |