![]() |
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 767 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓) | |
2 | 1 | 3ad2antl1 1182 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: soisores 7334 tfisi 7864 omopth2 8605 swrdsbslen 14658 swrdspsleq 14659 repswswrd 14778 ramub1lem1 17014 efgsfo 19723 lbspss 20996 maducoeval2 22603 madurid 22607 decpmatmullem 22734 mp2pm2mplem4 22772 llyrest 23450 ptbasin 23542 basqtop 23676 ustuqtop1 24207 mulcxp 26681 noetalem1 27740 sltmul2 28141 elwwlks2ons3im 29857 br8d 32499 isarchi2 33006 archiabllem2c 33016 cvmlift2lem10 35073 5segofs 35753 btwnconn1lem13 35846 2llnjaN 39189 paddasslem12 39454 lhp2lt 39624 lhpexle2lem 39632 lhpmcvr3 39648 lhpat3 39669 trlval3 39810 cdleme17b 39910 cdlemefr27cl 40026 cdlemg11b 40265 tendococl 40395 cdlemj3 40446 cdlemk35s-id 40561 cdlemk39s-id 40563 cdlemk53b 40579 cdlemk35u 40587 cdlemm10N 40741 dihopelvalcpre 40871 dihord6apre 40879 dihord5b 40882 dihglblem5apreN 40914 dihglblem2N 40917 dihmeetlem6 40932 dihmeetlem18N 40947 dvh3dim2 41071 dvh3dim3N 41072 jm2.25lem1 42566 limcleqr 45175 icccncfext 45418 fourierdlem87 45724 sge0seq 45977 smflimsuplem7 46357 fsupdm 46373 finfdm 46377 itscnhlc0xyqsol 48029 itscnhlinecirc02plem2 48047 |
Copyright terms: Public domain | W3C validator |