![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad4ant23 | 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 |
---|---|
ad4ant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
ad4ant23 | ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad4ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | adantr 480 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒) |
3 | 2 | adantlll 715 | 1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 206 df-an 396 |
This theorem is referenced by: fntpb 7213 suppssfv 8190 omsmolem 8659 ttukeylem5 10511 rlim3 15447 mp2pm2mplem4 22532 chfacfisf 22577 chfacfisfcpmat 22578 mbfi1fseqlem3 25468 usgredg2vlem2 28751 umgr3v3e3cycl 29705 matunitlindflem1 36788 matunitlindflem2 36789 heicant 36827 naddgeoa 42448 difmap 44205 xlimmnfvlem2 44848 xlimpnfvlem2 44852 xlimliminflimsup 44877 sge0resplit 45421 hoidmvle 45615 eenglngeehlnmlem2 47512 |
Copyright terms: Public domain | W3C validator |