![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adantl2 | 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 |
---|---|
3adantl2 | ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpb 1142 | . 2 ⊢ ((𝜑 ∧ 𝜏 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
2 | 3adantl.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 580 | 1 ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 |
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 208 df-an 397 df-3an 1082 |
This theorem is referenced by: 3ad2antl1 1178 omord2 8050 nnmord 8115 axcc3 9713 lediv2a 11388 zdiv 11906 clatleglb 17569 mulgnn0subcl 18000 mulgsubcl 18001 ghmmulg 18115 obs2ss 20559 scmatf1 20828 neiint 21400 cnpnei 21560 caublcls 23599 axlowdimlem16 26430 clwwlkext2edg 27521 ipval2lem2 28168 fh1 29082 cm2j 29084 hoadddi 29267 hoadddir 29268 lindsadd 34437 lautco 36785 supxrge 41168 infleinflem2 41201 stoweidlem44 41893 fourierdlem41 41997 fourierdlem42 41998 fourierdlem54 42009 fourierdlem83 42038 sge0uzfsumgt 42290 |
Copyright terms: Public domain | W3C validator |