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 1148 | . 2 ⊢ ((𝜏 ∧ 𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
2 | 3adantl.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 579 | 1 ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 396 df-3an 1087 |
This theorem is referenced by: 3ad2antl2 1184 3ad2antl3 1185 funcnvqp 6482 onfununi 8143 omord2 8360 en2eqpr 9694 divmuldiv 11605 ioojoin 13144 expnlbnd 13876 swrdlend 14294 2cshw 14454 lcmledvds 16232 pospropd 17960 marrepcl 21621 gsummatr01lem3 21714 upxp 22682 rnelfmlem 23011 brbtwn2 27176 wlkonprop 27928 trlsonprop 27977 pthsonprop 28013 spthonprop 28014 spthonepeq 28021 fh2 29882 homulass 30065 hoadddi 30066 hoadddir 30067 metf1o 35840 rngohomco 36059 rngoisoco 36067 op01dm 37124 paddss12 37760 wessf1ornlem 42611 elaa2 43665 smflimlem2 44194 |
Copyright terms: Public domain | W3C validator |