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 1141 | . 2 ⊢ ((𝜑 ∧ 𝜏 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
2 | 3adantl.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 580 | 1 ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 1081 |
This theorem is referenced by: 3ad2antl1 1177 omord2 8182 nnmord 8247 axcc3 9848 lediv2a 11522 zdiv 12040 clatleglb 17724 mulgnn0subcl 18179 mulgsubcl 18180 ghmmulg 18308 obs2ss 20801 scmatf1 21068 neiint 21640 cnpnei 21800 caublcls 23839 axlowdimlem16 26670 clwwlkext2edg 27762 ipval2lem2 28408 fh1 29322 cm2j 29324 hoadddi 29507 hoadddir 29508 lindsadd 34766 lautco 37113 supxrge 41482 infleinflem2 41515 stoweidlem44 42206 fourierdlem41 42310 fourierdlem42 42311 fourierdlem54 42322 fourierdlem83 42351 sge0uzfsumgt 42603 |
Copyright terms: Public domain | W3C validator |