![]() |
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 1137 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antrl 727 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: poxp2 8129 poxp3 8136 pwfseqlem1 10653 pwfseqlem5 10658 icodiamlt 15382 issubc3 17799 pgpfac1lem5 19949 clsconn 22934 txlly 23140 txnlly 23141 itg2add 25277 ftc1a 25554 nosupprefixmo 27203 noinfprefixmo 27204 nosupbnd2 27219 noinfbnd2 27234 mulsprop 27589 f1otrg 28153 ax5seglem6 28223 axcontlem9 28261 axcontlem10 28262 elwspths2spth 29252 wwlksext2clwwlk 29341 locfinref 32852 erdszelem7 34219 cvmlift2lem10 34334 btwnouttr2 35025 btwnconn1lem13 35102 broutsideof2 35125 mpaaeu 41940 dfsalgen2 45105 fundcmpsurinjpreimafv 46124 digexp 47341 line2xlem 47487 |
Copyright terms: Public domain | W3C validator |