Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simpl1r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpl1r | ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1r 1079 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | adantr 480 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: soisores 6477 tfisi 6950 omopth2 7551 swrdsbslen 13300 swrdspsleq 13301 repswswrd 13382 ramub1lem1 15568 efgsfo 17975 lbspss 18903 maducoeval2 20265 madurid 20269 decpmatmullem 20395 mp2pm2mplem4 20433 llyrest 21098 ptbasin 21190 basqtop 21324 ustuqtop1 21855 mulcxp 24231 br8d 28802 isarchi2 29070 archiabllem2c 29080 cvmlift2lem10 30548 5segofs 31283 btwnconn1lem13 31376 2llnjaN 33870 paddasslem12 34135 lhp2lt 34305 lhpexle2lem 34313 lhpmcvr3 34329 lhpat3 34350 trlval3 34492 cdleme17b 34592 cdlemefr27cl 34709 cdlemg11b 34948 tendococl 35078 cdlemj3 35129 cdlemk35s-id 35244 cdlemk39s-id 35246 cdlemk53b 35262 cdlemk35u 35270 cdlemm10N 35425 dihopelvalcpre 35555 dihord6apre 35563 dihord5b 35566 dihglblem5apreN 35598 dihglblem2N 35601 dihmeetlem6 35616 dihmeetlem18N 35631 dvh3dim2 35755 dvh3dim3N 35756 jm2.25lem1 36583 limcleqr 38711 icccncfext 38773 fourierdlem87 39086 sge0seq 39339 |
Copyright terms: Public domain | W3C validator |