![]() |
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 1149 | . 2 ⊢ ((𝜑 ∧ 𝜏 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
2 | 3adantl.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 580 | 1 ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: 3ad2antl1 1185 omord2 8513 nnmord 8578 axcc3 10373 lediv2a 12048 zdiv 12572 clatleglb 18406 mulgnn0subcl 18887 mulgsubcl 18888 ghmmulg 19018 obs2ss 21133 scmatf1 21878 neiint 22453 cnpnei 22613 caublcls 24671 axlowdimlem16 27904 clwwlkext2edg 28998 ipval2lem2 29644 fh1 30558 cm2j 30560 hoadddi 30743 hoadddir 30744 lindsadd 36062 lautco 38551 sticksstones1 40545 sticksstones12 40557 supxrge 43548 infleinflem2 43581 stoweidlem44 44257 fourierdlem41 44361 fourierdlem42 44362 fourierdlem54 44373 fourierdlem83 44402 sge0uzfsumgt 44657 |
Copyright terms: Public domain | W3C validator |