![]() |
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 791 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant2 1170 | 1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1113 |
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 1115 |
This theorem is referenced by: tfrlem5 7742 omeu 7932 gruina 9955 4sqlem18 16037 vdwlem10 16065 mdetuni0 20795 mdetmul 20797 tsmsxp 22328 ax5seglem3 26230 btwnconn1lem1 32733 btwnconn1lem3 32735 btwnconn1lem4 32736 btwnconn1lem5 32737 btwnconn1lem6 32738 btwnconn1lem7 32739 btwnconn1lem12 32744 linethru 32799 2llnjN 35642 2lplnja 35694 2lplnj 35695 cdlemblem 35868 dalaw 35961 pclfinN 35975 lhpmcvr4N 36101 cdlemb2 36116 cdleme01N 36296 cdleme0ex2N 36299 cdleme7c 36320 cdlemefrs29bpre0 36471 cdlemefrs29cpre1 36473 cdlemefrs32fva1 36476 cdlemefs32sn1aw 36489 cdleme41sn3a 36508 cdleme48fv 36574 cdlemk21-2N 36966 dihmeetlem13N 37394 pellex 38243 lmhmfgsplit 38499 iunrelexpmin1 38841 |
Copyright terms: Public domain | W3C validator |