|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simpr2l | 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 | 
|---|---|
| simpr2l | ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simprl 770 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
| 2 | 1 | 3ad2antr2 1189 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 | 
| 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 1088 | 
| This theorem is referenced by: poxp2 8169 ttrcltr 9757 ttrclss 9761 dmttrcl 9762 ttrclselem2 9767 oppccatid 17763 subccatid 17892 setccatid 18130 catccatid 18152 estrccatid 18177 xpccatid 18234 kerf1ghm 19266 gsmsymgreqlem1 19449 nllyidm 23498 noinfbnd1lem5 27773 ax5seg 28954 3pthdlem1 30184 segconeq 36012 ifscgr 36046 brofs2 36079 brifs2 36080 idinside 36086 btwnconn1lem8 36096 btwnconn1lem12 36100 segcon2 36107 segletr 36116 outsidele 36134 unbdqndv2 36513 lplnexllnN 39567 paddasslem9 39831 pmodlem2 39850 lhp2lt 40004 cdlemc3 40196 cdlemc4 40197 cdlemd1 40201 cdleme3b 40232 cdleme3c 40233 cdleme42ke 40488 cdlemg4c 40615 clnbgrgrimlem 47906 isthincd2 49111 mndtccatid 49239 | 
| Copyright terms: Public domain | W3C validator |