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 484 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒) |
3 | 2 | adantlll 718 | 1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 |
This theorem is referenced by: fntpb 7025 suppssfv 7944 omsmolem 8382 ttukeylem5 10127 rlim3 15059 mp2pm2mplem4 21706 chfacfisf 21751 chfacfisfcpmat 21752 mbfi1fseqlem3 24615 usgredg2vlem2 27314 umgr3v3e3cycl 28267 matunitlindflem1 35510 matunitlindflem2 35511 heicant 35549 difmap 42420 xlimmnfvlem2 43049 xlimpnfvlem2 43053 xlimliminflimsup 43078 sge0resplit 43619 hoidmvle 43813 eenglngeehlnmlem2 45757 |
Copyright terms: Public domain | W3C validator |