| 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 1150 | . 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: 3ad2antl1 1186 omord2 8605 nnmord 8670 axcc3 10478 lediv2a 12162 zdiv 12688 clatleglb 18563 mulgnn0subcl 19105 mulgsubcl 19106 ghmmulg 19246 obs2ss 21749 scmatf1 22537 neiint 23112 cnpnei 23272 caublcls 25343 axlowdimlem16 28972 clwwlkext2edg 30075 ipval2lem2 30723 fh1 31637 cm2j 31639 hoadddi 31822 hoadddir 31823 lindsadd 37620 lautco 40099 sticksstones1 42147 sticksstones12 42159 supxrge 45349 infleinflem2 45382 stoweidlem44 46059 fourierdlem41 46163 fourierdlem42 46164 fourierdlem54 46175 fourierdlem83 46204 sge0uzfsumgt 46459 |
| Copyright terms: Public domain | W3C validator |