![]() |
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 8080 poxp3 8087 pwfseqlem1 10601 pwfseqlem5 10606 icodiamlt 15327 issubc3 17742 pgpfac1lem5 19865 clsconn 22797 txlly 23003 txnlly 23004 itg2add 25140 ftc1a 25417 nosupprefixmo 27064 noinfprefixmo 27065 nosupbnd2 27080 noinfbnd2 27095 f1otrg 27855 ax5seglem6 27925 axcontlem9 27963 axcontlem10 27964 elwspths2spth 28954 wwlksext2clwwlk 29043 locfinref 32462 erdszelem7 33831 cvmlift2lem10 33946 btwnouttr2 34636 btwnconn1lem13 34713 broutsideof2 34736 mpaaeu 41506 dfsalgen2 44656 fundcmpsurinjpreimafv 45674 digexp 46767 line2xlem 46913 |
Copyright terms: Public domain | W3C validator |