| 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 1151 | . 2 ⊢ ((𝜏 ∧ 𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
| 2 | 3adantl.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
| 3 | 1, 2 | sylan 580 | 1 ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 1089 |
| This theorem is referenced by: 3ad2antl2 1187 3ad2antl3 1188 funcnvqp 6630 onfununi 8381 omord2 8605 en2eqpr 10047 divmuldiv 11967 ioojoin 13523 expnlbnd 14272 swrdlend 14691 2cshw 14851 lcmledvds 16636 pospropd 18372 marrepcl 22570 gsummatr01lem3 22663 upxp 23631 rnelfmlem 23960 brbtwn2 28920 wlkonprop 29676 trlsonprop 29726 pthsonprop 29764 spthonprop 29765 spthonepeq 29772 fh2 31638 homulass 31821 hoadddi 31822 hoadddir 31823 metf1o 37762 rngohomco 37981 rngoisoco 37989 op01dm 39184 paddss12 39821 wessf1ornlem 45190 elaa2 46249 smflimlem2 46787 |
| Copyright terms: Public domain | W3C validator |