![]() |
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 479 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒) |
3 | 2 | adantlll 714 | 1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: fntpb 7212 suppssfv 8189 omsmolem 8658 ttukeylem5 10510 rlim3 15446 mp2pm2mplem4 22531 chfacfisf 22576 chfacfisfcpmat 22577 mbfi1fseqlem3 25467 usgredg2vlem2 28750 umgr3v3e3cycl 29704 matunitlindflem1 36787 matunitlindflem2 36788 heicant 36826 naddgeoa 42447 difmap 44204 xlimmnfvlem2 44847 xlimpnfvlem2 44851 xlimliminflimsup 44876 sge0resplit 45420 hoidmvle 45614 eenglngeehlnmlem2 47511 |
Copyright terms: Public domain | W3C validator |