![]() |
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 759 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓) | |
2 | 1 | 3ad2antl1 1193 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: soisores 6851 tfisi 7338 omopth2 7950 swrdsbslen 13774 swrdspsleq 13775 repswswrd 13936 ramub1lem1 16145 efgsfo 18548 lbspss 19488 maducoeval2 20862 madurid 20866 decpmatmullem 20994 mp2pm2mplem4 21032 llyrest 21708 ptbasin 21800 basqtop 21934 ustuqtop1 22464 mulcxp 24879 elwwlks2ons3im 27351 br8d 30002 isarchi2 30309 archiabllem2c 30319 cvmlift2lem10 31901 5segofs 32710 btwnconn1lem13 32803 2llnjaN 35729 paddasslem12 35994 lhp2lt 36164 lhpexle2lem 36172 lhpmcvr3 36188 lhpat3 36209 trlval3 36350 cdleme17b 36450 cdlemefr27cl 36566 cdlemg11b 36805 tendococl 36935 cdlemj3 36986 cdlemk35s-id 37101 cdlemk39s-id 37103 cdlemk53b 37119 cdlemk35u 37127 cdlemm10N 37281 dihopelvalcpre 37411 dihord6apre 37419 dihord5b 37422 dihglblem5apreN 37454 dihglblem2N 37457 dihmeetlem6 37472 dihmeetlem18N 37487 dvh3dim2 37611 dvh3dim3N 37612 jm2.25lem1 38538 limcleqr 40798 icccncfext 41042 fourierdlem87 41351 sge0seq 41601 smflimsuplem7 41973 itscnhlc0xyqsol 43515 itscnhlinecirc02plem2 43533 |
Copyright terms: Public domain | W3C validator |