![]() |
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 1135 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | 1 | ad2antrl 728 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: poxp2 8167 poxp3 8174 pwfseqlem1 10696 pwfseqlem5 10701 icodiamlt 15471 issubc3 17900 pgpfac1lem5 20114 clsconn 23454 txlly 23660 txnlly 23661 itg2add 25809 ftc1a 26093 nosupprefixmo 27760 noinfprefixmo 27761 nosupbnd2 27776 noinfbnd2 27791 mulsprop 28171 f1otrg 28894 ax5seglem6 28964 axcontlem9 29002 axcontlem10 29003 elwspths2spth 29997 wwlksext2clwwlk 30086 locfinref 33802 erdszelem7 35182 cvmlift2lem10 35297 btwnouttr2 36004 btwnconn1lem13 36081 broutsideof2 36104 mpaaeu 43139 dfsalgen2 46297 fundcmpsurinjpreimafv 47333 grtrimap 47851 digexp 48457 line2xlem 48603 |
Copyright terms: Public domain | W3C validator |