![]() |
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 1147 | . 2 ⊢ ((𝜏 ∧ 𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
2 | 3adantl.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 578 | 1 ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: 3ad2antl2 1183 3ad2antl3 1184 funcnvqp 6615 onfununi 8363 omord2 8589 en2eqpr 10043 divmuldiv 11959 ioojoin 13508 expnlbnd 14245 swrdlend 14656 2cshw 14816 lcmledvds 16595 pospropd 18347 marrepcl 22554 gsummatr01lem3 22647 upxp 23615 rnelfmlem 23944 brbtwn2 28836 wlkonprop 29592 trlsonprop 29642 pthsonprop 29678 spthonprop 29679 spthonepeq 29686 fh2 31549 homulass 31732 hoadddi 31733 hoadddir 31734 metf1o 37469 rngohomco 37688 rngoisoco 37696 op01dm 38894 paddss12 39531 wessf1ornlem 44828 elaa2 45891 smflimlem2 46429 |
Copyright terms: Public domain | W3C validator |