Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3adant2l | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
3adant1l.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant2l | ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3adant1l.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3com12 1261 | . . 3 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
3 | 2 | 3adant1l 1310 | . 2 ⊢ (((𝜏 ∧ 𝜓) ∧ 𝜑 ∧ 𝜒) → 𝜃) |
4 | 3 | 3com12 1261 | 1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: axdc3lem4 9158 modexp 12861 lmmbr2 22865 ax5seglem1 25608 ax5seglem2 25609 nvaddsub4 26896 pl1cn 29329 athgt 33760 ltrncoelN 34447 ltrncoat 34448 trlcoabs 35027 tendoplcl2 35084 tendopltp 35086 dih1dimatlem0 35635 pellex 36417 fourierdlem42 39042 |
Copyright terms: Public domain | W3C validator |