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 1131 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antrl 726 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1082 |
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 209 df-an 399 df-3an 1084 |
This theorem is referenced by: pwfseqlem1 10072 pwfseqlem5 10077 icodiamlt 14787 issubc3 17111 pgpfac1lem5 19193 clsconn 22030 txlly 22236 txnlly 22237 itg2add 24352 ftc1a 24626 f1otrg 26649 ax5seglem6 26712 axcontlem9 26750 axcontlem10 26751 elwspths2spth 27738 wwlksext2clwwlk 27828 locfinref 31098 erdszelem7 32437 cvmlift2lem10 32552 noprefixmo 33195 nosupbnd2 33209 btwnouttr2 33476 btwnconn1lem13 33553 broutsideof2 33576 mpaaeu 39741 dfsalgen2 42615 fundcmpsurinjpreimafv 43559 digexp 44658 line2xlem 44731 |
Copyright terms: Public domain | W3C validator |