![]() |
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 772 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant2 1132 | 1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 396 df-3an 1087 |
This theorem is referenced by: fpr3g 8290 tfrlem5 8400 omeu 8605 gruina 10841 4sqlem18 16930 vdwlem10 16958 mdetuni0 22522 mdetmul 22524 tsmsxp 24058 ax5seglem3 28741 btwnconn1lem1 35683 btwnconn1lem3 35685 btwnconn1lem4 35686 btwnconn1lem5 35687 btwnconn1lem6 35688 btwnconn1lem7 35689 btwnconn1lem12 35694 linethru 35749 2llnjN 39040 2lplnja 39092 2lplnj 39093 cdlemblem 39266 dalaw 39359 pclfinN 39373 lhpmcvr4N 39499 cdlemb2 39514 cdleme01N 39694 cdleme0ex2N 39697 cdleme7c 39718 cdlemefrs29bpre0 39869 cdlemefrs29cpre1 39871 cdlemefrs32fva1 39874 cdlemefs32sn1aw 39887 cdleme41sn3a 39906 cdleme48fv 39972 cdlemk21-2N 40364 dihmeetlem13N 40792 pellex 42255 lmhmfgsplit 42510 iunrelexpmin1 43138 |
Copyright terms: Public domain | W3C validator |