Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3adant1l | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
3adant1l.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant1l | ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3adant1l.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3expb 1266 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
3 | 2 | adantll 750 | . 2 ⊢ (((𝜏 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
4 | 3 | 3impb 1260 | 1 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: 3adant2l 1320 3adant3l 1322 cfsmolem 9092 axdc3lem4 9275 issubmnd 17318 maducoeval2 20446 cramerlem3 20495 restnlly 21285 efgh 24287 funvtxdm2valOLD 25895 funiedgdm2valOLD 25896 hasheuni 30147 matunitlindflem1 33405 pellex 37399 mendlmod 37763 disjf1o 39378 ssfiunibd 39523 mullimc 39848 mullimcf 39855 limclner 39883 limsupresxr 39998 liminfresxr 39999 sge0lefi 40615 isomenndlem 40744 hoicvr 40762 ovncvrrp 40778 |
Copyright terms: Public domain | W3C validator |