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 769 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant2 1126 | 1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: tfrlem5 8005 omeu 8200 gruina 10228 4sqlem18 16286 vdwlem10 16314 mdetuni0 21158 mdetmul 21160 tsmsxp 22690 ax5seglem3 26644 fpr3g 33019 btwnconn1lem1 33445 btwnconn1lem3 33447 btwnconn1lem4 33448 btwnconn1lem5 33449 btwnconn1lem6 33450 btwnconn1lem7 33451 btwnconn1lem12 33456 linethru 33511 2llnjN 36583 2lplnja 36635 2lplnj 36636 cdlemblem 36809 dalaw 36902 pclfinN 36916 lhpmcvr4N 37042 cdlemb2 37057 cdleme01N 37237 cdleme0ex2N 37240 cdleme7c 37261 cdlemefrs29bpre0 37412 cdlemefrs29cpre1 37414 cdlemefrs32fva1 37417 cdlemefs32sn1aw 37430 cdleme41sn3a 37449 cdleme48fv 37515 cdlemk21-2N 37907 dihmeetlem13N 38335 pellex 39310 lmhmfgsplit 39564 iunrelexpmin1 39931 |
Copyright terms: Public domain | W3C validator |