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 481 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒) |
3 | 2 | adantlll 714 | 1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: fntpb 6963 suppssfv 7855 omsmolem 8269 ttukeylem5 9923 rlim3 14843 mp2pm2mplem4 21345 chfacfisf 21390 chfacfisfcpmat 21391 mbfi1fseqlem3 24245 usgredg2vlem2 26935 umgr3v3e3cycl 27890 matunitlindflem1 34769 matunitlindflem2 34770 heicant 34808 difmap 41346 xlimmnfvlem2 41990 xlimpnfvlem2 41994 xlimliminflimsup 42019 sge0resplit 42565 hoidmvle 42759 eenglngeehlnmlem2 44653 |
Copyright terms: Public domain | W3C validator |