![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simprl1 | 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 |
---|---|
simprl1 | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 1136 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antrl 726 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: poxp2 8128 poxp3 8135 pwfseqlem1 10652 pwfseqlem5 10657 icodiamlt 15381 issubc3 17798 pgpfac1lem5 19948 clsconn 22933 txlly 23139 txnlly 23140 itg2add 25276 ftc1a 25553 nosupprefixmo 27200 noinfprefixmo 27201 nosupbnd2 27216 noinfbnd2 27231 mulsprop 27583 f1otrg 28119 ax5seglem6 28189 axcontlem9 28227 axcontlem10 28228 elwspths2spth 29218 wwlksext2clwwlk 29307 locfinref 32816 erdszelem7 34183 cvmlift2lem10 34298 btwnouttr2 34989 btwnconn1lem13 35066 broutsideof2 35089 mpaaeu 41882 dfsalgen2 45047 fundcmpsurinjpreimafv 46066 digexp 47283 line2xlem 47429 |
Copyright terms: Public domain | W3C validator |