| 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.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
| Ref | Expression |
|---|---|
| simpl1r | ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simplr 769 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓) | |
| 2 | 1 | 3ad2antl1 1186 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 1089 |
| This theorem is referenced by: soisores 7347 tfisi 7880 omopth2 8622 swrdsbslen 14702 swrdspsleq 14703 repswswrd 14822 ramub1lem1 17064 efgsfo 19757 lbspss 21081 maducoeval2 22646 madurid 22650 decpmatmullem 22777 mp2pm2mplem4 22815 llyrest 23493 ptbasin 23585 basqtop 23719 ustuqtop1 24250 mulcxp 26727 noetalem1 27786 sltmul2 28197 elwwlks2ons3im 29974 br8d 32622 isarchi2 33192 archiabllem2c 33202 cvmlift2lem10 35317 5segofs 36007 btwnconn1lem13 36100 2llnjaN 39568 paddasslem12 39833 lhp2lt 40003 lhpexle2lem 40011 lhpmcvr3 40027 lhpat3 40048 trlval3 40189 cdleme17b 40289 cdlemefr27cl 40405 cdlemg11b 40644 tendococl 40774 cdlemj3 40825 cdlemk35s-id 40940 cdlemk39s-id 40942 cdlemk53b 40958 cdlemk35u 40966 cdlemm10N 41120 dihopelvalcpre 41250 dihord6apre 41258 dihord5b 41261 dihglblem5apreN 41293 dihglblem2N 41296 dihmeetlem6 41311 dihmeetlem18N 41326 dvh3dim2 41450 dvh3dim3N 41451 jm2.25lem1 43010 limcleqr 45659 icccncfext 45902 fourierdlem87 46208 sge0seq 46461 smflimsuplem7 46841 fsupdm 46857 finfdm 46861 itscnhlc0xyqsol 48686 itscnhlinecirc02plem2 48704 |
| Copyright terms: Public domain | W3C validator |