![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad4ant124 | Structured version Visualization version GIF version |
Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
Ref | Expression |
---|---|
ad4ant3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
ad4ant124 | ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad4ant3.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3expa 1115 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | adantlr 714 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1084 |
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 1086 |
This theorem is referenced by: ad5ant124 1362 ixxin 12743 odf1 18681 m2cpmfo 21361 cnflf 22607 cnfcf 22647 tmdmulg 22697 blin 23028 blsscls2 23111 metcn 23150 xrsxmet 23414 sqf11 25724 dimval 31089 dfgcd3 34738 lindsadd 35050 hspmbllem2 43266 |
Copyright terms: Public domain | W3C validator |