![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adantl1 | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
Ref | Expression |
---|---|
3adantl.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adantl1 | ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpc 1143 | . 2 ⊢ ((𝜏 ∧ 𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
2 | 3adantl.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 575 | 1 ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: 3ad2antl2 1194 3ad2antl3 1195 funcnvqp 6198 onfununi 7721 omord2 7931 en2eqpr 9163 divmuldiv 11075 ioojoin 12620 expnlbnd 13313 swrdlend 13748 lcmledvds 15718 pospropd 17520 marrepcl 20775 gsummatr01lem3 20869 upxp 21835 rnelfmlem 22164 brbtwn2 26254 spthonepeq 27104 fh2 29050 homulass 29233 hoadddi 29234 hoadddir 29235 metf1o 34175 rngohomco 34397 rngoisoco 34405 op01dm 35337 paddss12 35973 wessf1ornlem 40294 elaa2 41378 smflimlem2 41907 |
Copyright terms: Public domain | W3C validator |