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 1151 | . 2 ⊢ ((𝜑 ∧ 𝜏 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
2 | 3adantl.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 583 | 1 ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: 3ad2antl1 1187 omord2 8292 nnmord 8357 axcc3 10049 lediv2a 11723 zdiv 12244 clatleglb 18021 mulgnn0subcl 18502 mulgsubcl 18503 ghmmulg 18631 obs2ss 20688 scmatf1 21425 neiint 21998 cnpnei 22158 caublcls 24203 axlowdimlem16 27045 clwwlkext2edg 28136 ipval2lem2 28782 fh1 29696 cm2j 29698 hoadddi 29881 hoadddir 29882 lindsadd 35505 lautco 37846 sticksstones1 39822 sticksstones12 39834 supxrge 42548 infleinflem2 42581 stoweidlem44 43258 fourierdlem41 43362 fourierdlem42 43363 fourierdlem54 43374 fourierdlem83 43403 sge0uzfsumgt 43655 |
Copyright terms: Public domain | W3C validator |