| 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 728 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: poxp2 8168 poxp3 8175 pwfseqlem1 10698 pwfseqlem5 10703 icodiamlt 15474 issubc3 17894 pgpfac1lem5 20099 clsconn 23438 txlly 23644 txnlly 23645 itg2add 25794 ftc1a 26078 nosupprefixmo 27745 noinfprefixmo 27746 nosupbnd2 27761 noinfbnd2 27776 mulsprop 28156 f1otrg 28879 ax5seglem6 28949 axcontlem9 28987 axcontlem10 28988 elwspths2spth 29987 wwlksext2clwwlk 30076 locfinref 33840 erdszelem7 35202 cvmlift2lem10 35317 btwnouttr2 36023 btwnconn1lem13 36100 broutsideof2 36123 mpaaeu 43162 dfsalgen2 46356 fundcmpsurinjpreimafv 47395 grtrimap 47915 digexp 48528 line2xlem 48674 |
| Copyright terms: Public domain | W3C validator |