![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpr2r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
Ref | Expression |
---|---|
simpr2r | ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprr 772 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2antr2 1190 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: poxp2 8076 poxp3 8083 frrlem8 8225 ttrcltr 9657 ttrclss 9661 rnttrcl 9663 ttrclselem2 9667 oppccatid 17606 subccatid 17737 setccatid 17975 catccatid 17997 estrccatid 18024 xpccatid 18081 gsmsymgreqlem1 19217 kerf1ghm 20184 ax5seg 27929 3pthdlem1 29150 segconeq 34641 ifscgr 34675 brofs2 34708 brifs2 34709 idinside 34715 btwnconn1lem8 34725 btwnconn1lem11 34728 btwnconn1lem12 34729 segcon2 34736 seglecgr12im 34741 unbdqndv2 35020 lplnexllnN 38073 paddasslem9 38337 paddasslem15 38343 pmodlem2 38356 lhp2lt 38510 isthincd2 47144 mndtccatid 47199 |
Copyright terms: Public domain | W3C validator |